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.

7 files changed, 14 insertions, 11 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index f0c7b5a7f..714192f53 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -988,7 +988,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
     (mk_equation_id f_id)
     (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem))
     (lemma_type, (*FIXME*) Univ.ContextSet.empty)
-    (fun _ _ -> ());
+    (Future.mk_hook (fun _ _ -> ()));
   ignore (Pfedit.by (Proofview.V82.tactic prove_replacement));
   Lemmas.save_proof (Vernacexpr.Proved(false,None))
 
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
 
 
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 70a892a3b..8c8d7a667 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -352,7 +352,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
     | [((_,fname),_,bl,ret_type,body),_] when not is_rec ->
       let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in 
 	Command.do_definition fname (Decl_kinds.Global,(*FIXME*)false,Decl_kinds.Definition)
-	  bl None body (Some ret_type) (fun _ _ -> ())
+	  bl None body (Some ret_type) (Future.mk_hook (fun _ _ -> ()))
     | _ ->
 	Command.do_fixpoint Global false(*FIXME*) fixpoint_exprl
 
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
 
 
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 6e8b79a6b..3fafeadc1 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -46,7 +46,7 @@ val const_of_id: Id.t -> constant
 val jmeq : unit -> Term.constr
 val jmeq_refl : unit -> Term.constr
 
-val save : bool -> Id.t ->  Entries.definition_entry  -> Decl_kinds.goal_kind ->
+val save : bool -> Id.t -> Entries.definition_entry  -> Decl_kinds.goal_kind ->
   unit Tacexpr.declaration_hook Ephemeron.key -> unit
 
 (* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index d5640798e..9558923f6 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))));
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 439014361..08d8ca391 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1320,7 +1320,7 @@ let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompos
     na
     (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma)
     (gls_type, ctx)
-    hook;
+    (Future.mk_hook hook);
   if Indfun_common.is_strict_tcc  ()
   then
     ignore (by (Proofview.V82.tactic (tclIDTAC)))
@@ -1415,7 +1415,9 @@ let (com_eqn : int -> Id.t ->
     let f_constr = constr_of_global f_ref in
     let equation_lemma_type = subst1 f_constr equation_lemma_type in
     (Lemmas.start_proof eq_name (Global, false, Proof Lemma)
-       ~sign:(Environ.named_context_val env) (equation_lemma_type, (*FIXME*)Univ.ContextSet.empty) (fun _ _ -> ());
+       ~sign:(Environ.named_context_val env)
+       (equation_lemma_type, (*FIXME*)Univ.ContextSet.empty)
+       (Future.mk_hook (fun _ _ -> ()));
      ignore (by
        (Proofview.V82.tactic (start_equation f_ref terminate_ref
 	  (fun  x ->
@@ -1535,5 +1537,5 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
       term_id
       using_lemmas
       (List.length res_vars)
-      ctx hook)
+      ctx (Future.mk_hook hook))
     ()