Commit 959edfa9 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

minor

parent b26ae3d8
...@@ -125,17 +125,17 @@ exception GoalFound ...@@ -125,17 +125,17 @@ exception GoalFound
exception GoalNotFound exception GoalNotFound
let find_goal = function let find_goal = function
| Some {task_decl = {td_node = Decl {d_node = Dprop (Pgoal,p,f)}}} -> | Some {task_decl = {td_node = Decl {d_node = Dprop (Pgoal,p,f)}}} ->
Some(p,f) Some(p,f)
| _ -> None | _ -> None
let task_goal task = match find_goal task with let task_goal task = match find_goal task with
| Some(pr,_) -> pr | Some (pr,_) -> pr
| None -> raise GoalNotFound | None -> raise GoalNotFound
let task_goal_fmla task = match find_goal task with let task_goal_fmla task = match find_goal task with
| Some(_,f) -> f | Some (_,f) -> f
| None -> raise GoalNotFound | None -> raise GoalNotFound
let check_task task = match find_goal task with let check_task task = match find_goal task with
| Some _ -> raise GoalFound | Some _ -> raise GoalFound
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment