Moving hook code from Future to Lemmas. This seemed to disrupt compilation of

the checker, and it was not used before that anyway.

3 files changed, 21 insertions, 5 deletions

diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 493b874aed..5f580bca5e 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -32,6 +32,14 @@ open Constrexpr
 open Constrintern
 open Impargs
 
+type 'a declaration_hook = Decl_kinds.locality -> Globnames.global_reference -> 'a
+let mk_hook hook = hook
+let call_hook fix_exn hook l c =
+  try hook l c
+  with e when Errors.noncritical e ->
+    let e = Errors.push e in
+    raise (fix_exn e)
+
 (* Support for mutually proved theorems *)
 
 let retrieve_first_recthm = function
@@ -184,7 +192,7 @@ let save id const cstrs do_guard (locality,poly,kind) hook =
         let kn = declare_constant id ~local (DefinitionEntry const, k) in
 	(locality, ConstRef kn) in
   definition_message id;
-  Future.call_hook fix_exn hook l r
+  call_hook fix_exn hook l r
 
 let default_thm_id = Id.of_string "Unnamed_thm"
 
@@ -286,7 +294,7 @@ let admit hook () =
       str "declared as an axiom.")
   in
   let () = assumption_message id in
-  Future.call_hook (fun exn -> exn) hook Global (ConstRef kn)
+  call_hook (fun exn -> exn) hook Global (ConstRef kn)
 
 (* Starting a goal *)
 
@@ -401,8 +409,8 @@ let start_proof_with_initialization kind recguard thms snl hook =
         let thms_data = (strength,ref,imps)::other_thms_data in
         List.iter (fun (strength,ref,imps) ->
 	  maybe_declare_manual_implicits false ref imps;
-	  Future.call_hook (fun exn -> exn) hook strength ref) thms_data in
-      start_proof id kind t ?init_tac (Future.mk_hook hook) ~compute_guard:guard
+	  call_hook (fun exn -> exn) hook strength ref) thms_data in
+      start_proof id kind t ?init_tac (mk_hook hook) ~compute_guard:guard
 
 let start_proof_com kind thms hook =
   let env0 = Global.env () in
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
index 8f5c75976a..d0dd2d3336 100644
--- a/stm/lemmas.mli
+++ b/stm/lemmas.mli
@@ -14,6 +14,14 @@ open Tacexpr
 open Vernacexpr
 open Pfedit
 
+type 'a declaration_hook
+
+val mk_hook :
+  (Decl_kinds.locality -> Globnames.global_reference -> 'a) -> 'a declaration_hook
+
+val call_hook :
+  Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> Globnames.global_reference -> 'a
+
 (** A hook start_proof calls on the type of the definition being started *)
 val set_start_hook : (types -> unit) -> unit
 
diff --git a/stm/stm.ml b/stm/stm.ml
index c708389908..5733b0c321 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -764,7 +764,7 @@ end = struct
           (* The original terminator, a hook, has not been saved in the .vi*)
           Proof_global.set_terminator
             (Lemmas.standard_proof_terminator []
-              (Future.mk_hook (fun _ _ -> ())));
+              (Lemmas.mk_hook (fun _ _ -> ())));
           let proof = Proof_global.close_proof (fun x -> x) in
           vernac_interp eop ~proof
             { verbose = false; loc;