Commit d2b3d38a authored by Andrei Paskevich's avatar Andrei Paskevich

forbid Plemma's in tasks

parent 5e277d96
......@@ -166,16 +166,21 @@ let mk_task decl prev known = Htask.hashcons {
task_tag = -1;
}
exception LemmaFound
exception GoalFound
let push_decl task d =
begin match d.d_node with
| Dprop (Plemma,_,_) -> raise LemmaFound
| _ -> ()
end;
begin match task.task_decl.d_node with
| Dprop (Pgoal,_,_) -> raise GoalFound
| _ -> ()
end;
try
let kn = add_decl task.task_known d in
ignore (check_decl kn d);
begin match task.task_decl.d_node with
| Dprop (Pgoal,_,_) -> raise GoalFound
| _ -> ()
end;
mk_task d (Some task) kn
with DejaVu -> task
......
......@@ -65,4 +65,5 @@ exception UnknownIdent of ident
exception RedeclaredIdent of ident
exception GoalNotFound
exception GoalFound
exception LemmaFound
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