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/indfun_common.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/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 0d1e600ee..b923260c2 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -147,6 +147,7 @@ let get_locality = function | Global -> false let save with_clean id const (locality,_,kind) hook = + let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in let l,r = match locality with | Discharge when Lib.sections_are_opened () -> let k = Kindops.logical_kind_of_goal_kind kind in @@ -160,7 +161,7 @@ let save with_clean id const (locality,_,kind) hook = (locality, ConstRef kn) in if with_clean then Pfedit.delete_current_proof (); - Ephemeron.iter_opt hook (fun f -> f l r); + Ephemeron.iter_opt hook (fun f -> Future.call_hook fix_exn f l r); definition_message id |