From 289b2b9a1c3d3ebc3c1975663d16c04e88b6329b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 2 Jun 2014 10:52:31 +0200 Subject: 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. --- plugins/funind/functional_principles_types.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/funind/functional_principles_types.ml') diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index a8876c75b..65a262707 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -290,7 +290,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro let new_princ_name = next_ident_away_in_goal (Id.of_string "___________princ_________") [] in - let hook = hook new_principle_type in + let hook = Future.mk_hook (hook new_principle_type) in begin Lemmas.start_proof new_princ_name @@ -305,7 +305,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro (* let dur1 = System.time_difference tim1 tim2 in *) (* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *) (* end; *) - get_proof_clean true,Ephemeron.create hook + get_proof_clean true, Ephemeron.create hook end -- cgit v1.2.3