Commit 8db497e0 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

minor

parent 63ff46b1
...@@ -126,6 +126,10 @@ let check_decl kn d = match d.d_node with ...@@ -126,6 +126,10 @@ let check_decl kn d = match d.d_node with
| Dind dl -> List.iter (check_ind kn) dl | Dind dl -> List.iter (check_ind kn) dl
| Dprop (_,_,f) -> known_fmla kn f | Dprop (_,_,f) -> known_fmla kn f
let add_decl kn d =
let kn = add_decl kn d in
ignore (check_decl kn d);
kn
(** Task *) (** Task *)
...@@ -170,28 +174,22 @@ exception LemmaFound ...@@ -170,28 +174,22 @@ exception LemmaFound
exception GoalFound exception GoalFound
let push_decl task d = let push_decl task d =
begin match d.d_node with
| Dprop (Plemma,_,_) -> raise LemmaFound
| _ -> ()
end;
begin match task.task_decl.d_node with begin match task.task_decl.d_node with
| Dprop (Pgoal,_,_) -> raise GoalFound | Dprop (Pgoal,_,_) -> raise GoalFound
| _ -> () | _ -> ()
end; end;
try try mk_task d (Some task) (add_decl task.task_known d)
let kn = add_decl task.task_known d in
ignore (check_decl kn d);
mk_task d (Some task) kn
with DejaVu -> task with DejaVu -> task
let init_decl d = let init_decl d =
try try mk_task d None (add_decl Mid.empty d)
let kn = add_decl Mid.empty d in
ignore (check_decl kn d);
mk_task d None kn
with DejaVu -> assert false with DejaVu -> assert false
let add_decl opt d = let add_decl opt d =
begin match d.d_node with
| Dprop (Plemma,_,_) -> raise LemmaFound
| _ -> ()
end;
match opt with match opt with
| Some task -> Some (push_decl task d) | Some task -> Some (push_decl task d)
| None -> Some (init_decl d) | None -> Some (init_decl d)
......
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