diff options
| author | Enrico Tassi | 2014-06-02 10:52:31 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-06-08 11:17:05 +0200 |
| commit | 289b2b9a1c3d3ebc3c1975663d16c04e88b6329b (patch) | |
| tree | b8484b831d9fe3d027c186ebe86acbc82426fea3 /plugins/funind/invfun.ml | |
| parent | e1ba72037191b1d4be9de8a0a8fc1faa24eeb12c (diff) | |
Enforce a correct exception handling in declaration_hooks
This should finally get rid of the following class of bugs:
Qed fails, STM undoes to the beginning of the proof because the
exception is not annotated with the correct state, PG gets out of
sync because errors always refer to the last command in PGIP.
Diffstat (limited to 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index d5640798e2..9558923f6b 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -1080,7 +1080,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g Lemmas.start_proof lem_id (Decl_kinds.Global,false(*FIXME*),(Decl_kinds.Proof Decl_kinds.Theorem)) (fst lemmas_types_infos.(i), (*FIXME*)Univ.ContextSet.empty) - (fun _ _ -> ()); + (Future.mk_hook (fun _ _ -> ())); ignore (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")") (proving_tac i)))); @@ -1133,7 +1133,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g Lemmas.start_proof lem_id (Decl_kinds.Global,false(*FIXME*),(Decl_kinds.Proof Decl_kinds.Theorem)) (fst lemmas_types_infos.(i), (*FIXME*)Univ.ContextSet.empty) - (fun _ _ -> ()); + (Future.mk_hook (fun _ _ -> ())); ignore (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") (proving_tac i)))); |