diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-06-02 10:52:31 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-06-08 11:17:05 +0200 |
| commit | 289b2b9a1c3d3ebc3c1975663d16c04e88b6329b (patch) | |
| tree | b8484b831d9fe3d027c186ebe86acbc82426fea3 /plugins/funind/functional_principles_types.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/functional_principles_types.ml')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |