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

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

8 files changed, 27 insertions, 27 deletions

diff --git a/toplevel/class.ml b/toplevel/class.ml
index 1d85290511..635b1c52c0 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -304,7 +304,7 @@ let add_coercion_hook poly local ref =
   let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in
   Flags.if_verbose msg_info msg
 
-let add_coercion_hook poly = Future.mk_hook (add_coercion_hook poly)
+let add_coercion_hook poly = Lemmas.mk_hook (add_coercion_hook poly)
 
 let add_subclass_hook poly local ref =
   let stre = match local with
@@ -315,4 +315,4 @@ let add_subclass_hook poly local ref =
   let cl = class_of_global ref in
   try_add_new_coercion_subclass cl stre poly
 
-let add_subclass_hook poly = Future.mk_hook (add_subclass_hook poly)
+let add_subclass_hook poly = Lemmas.mk_hook (add_subclass_hook poly)
diff --git a/toplevel/class.mli b/toplevel/class.mli
index d472bd984a..d374610c35 100644
--- a/toplevel/class.mli
+++ b/toplevel/class.mli
@@ -41,8 +41,8 @@ val try_add_new_coercion_with_source : global_reference -> local:bool ->
 val try_add_new_identity_coercion : Id.t -> local:bool -> 
   Decl_kinds.polymorphic -> source:cl_typ -> target:cl_typ -> unit
 
-val add_coercion_hook : Decl_kinds.polymorphic -> unit Tacexpr.declaration_hook
+val add_coercion_hook : Decl_kinds.polymorphic -> unit Lemmas.declaration_hook
 
-val add_subclass_hook : Decl_kinds.polymorphic -> unit Tacexpr.declaration_hook
+val add_subclass_hook : Decl_kinds.polymorphic -> unit Lemmas.declaration_hook
 
 val class_of_global : global_reference -> cl_typ
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 5d1a0a43b6..99c3e977c0 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -294,7 +294,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 		  in obls, Some constr, typ
 		| None -> [||], None, termtype
 	      in
-              let hook = Future.mk_hook hook in
+              let hook = Lemmas.mk_hook hook in
 	      let ctx = Evd.universe_context_set evm in
 		ignore (Obligations.add_definition id ?term:constr
 			typ ctx ~kind:(Global,poly,Instance) ~hook obls);
@@ -303,7 +303,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 	      (Flags.silently 
 	       (fun () ->
 		Lemmas.start_proof id kind (termtype, Evd.universe_context_set evm)
-		(Future.mk_hook
+		(Lemmas.mk_hook
                   (fun _ -> instance_hook k pri global imps ?hook));
                  (* spiwack: I don't know what to do with the status here. *)
 		if not (Option.is_empty term) then 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index b49fe40a09..39fe8f4ab3 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -163,7 +163,7 @@ let declare_definition ident (local, p, k) ce imps hook =
     VarRef ident
   | Discharge | Local | Global ->
     declare_global_definition ident ce local k imps in
-  Future.call_hook (Future.fix_exn_of ce.Entries.const_entry_body) hook local r
+  Lemmas.call_hook (Future.fix_exn_of ce.Entries.const_entry_body) hook local r
 
 let _ = Obligations.declare_definition_ref := declare_definition
 
@@ -187,8 +187,8 @@ let do_definition ident k bl red_option c ctypopt hook =
           ident ~term:c cty ctx ~implicits:imps ~kind:k ~hook obls)
     else let ce = check_definition def in
       ignore(declare_definition ident k ce imps
-        (Future.mk_hook
-          (fun l r -> Future.call_hook (fun exn -> exn) hook l r;r)))
+        (Lemmas.mk_hook
+          (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r)))
 
 (* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
 
@@ -692,7 +692,7 @@ let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
 
 let declare_fix (_,poly,_ as kind) ctx f ((def,_),eff) t imps =
   let ce = definition_entry ~types:t ~poly ~univs:ctx ~eff def in
-  declare_definition f kind ce imps (Future.mk_hook (fun _ r -> r))
+  declare_definition f kind ce imps (Lemmas.mk_hook (fun _ r -> r))
 
 let _ = Obligations.declare_fix_ref := declare_fix
 
@@ -900,7 +900,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
 	  Impargs.declare_manual_implicits false gr [impls]
       in hook, recname, typ
   in
-  let hook = Future.mk_hook hook in
+  let hook = Lemmas.mk_hook hook in
   let fullcoqc = Evarutil.nf_evar !evdref def in
   let fullctyp = Evarutil.nf_evar !evdref typ in
   Obligations.check_evars env !evdref;
@@ -994,7 +994,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexe
       Option.map (List.map Proofview.V82.tactic) init_tac
     in
     Lemmas.start_proof_with_initialization (Global,poly,DefinitionBody Fixpoint)
-      (Some(false,indexes,init_tac)) thms None (Future.mk_hook (fun _ _ -> ()))
+      (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
   else begin
     (* We shortcut the proof process *)
     let fixdefs = List.map Option.get fixdefs in
@@ -1028,7 +1028,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns
       Option.map (List.map Proofview.V82.tactic) init_tac
     in
     Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint)
-      (Some(true,[],init_tac)) thms None (Future.mk_hook (fun _ _ -> ()))
+      (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
   else begin
     (* We shortcut the proof process *)
     let fixdefs = List.map Option.get fixdefs in
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 41cb5baa3b..e48a770009 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -34,11 +34,11 @@ val interp_definition :
 
 val declare_definition : Id.t -> definition_kind ->
   definition_entry -> Impargs.manual_implicits ->
-    Globnames.global_reference declaration_hook -> Globnames.global_reference
+    Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference
 
 val do_definition : Id.t -> definition_kind ->
   local_binder list -> red_expr option -> constr_expr ->
-  constr_expr option -> unit declaration_hook -> unit
+  constr_expr option -> unit Lemmas.declaration_hook -> unit
 
 (** {6 Parameters/Assumptions} *)
 
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 00fc3e0ce1..1543c5e875 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -333,7 +333,7 @@ type program_info = {
   prg_notations : notations ;
   prg_kind : definition_kind;
   prg_reduce : constr -> constr;
-  prg_hook : unit Tacexpr.declaration_hook;
+  prg_hook : unit Lemmas.declaration_hook;
 }
 
 let assumption_message = Declare.assumption_message
@@ -535,8 +535,8 @@ let declare_definition prg =
     progmap_remove prg;
     !declare_definition_ref prg.prg_name 
       prg.prg_kind ce prg.prg_implicits
-      (Future.mk_hook (fun l r ->
-         Future.call_hook (fun exn -> exn) prg.prg_hook l r; r))
+      (Lemmas.mk_hook (fun l r ->
+         Lemmas.call_hook (fun exn -> exn) prg.prg_hook l r; r))
 
 open Pp
 
@@ -607,7 +607,7 @@ let declare_mutual_definition l =
     Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
     let gr = List.hd kns in
     let kn = match gr with ConstRef kn -> kn | _ -> assert false in
-      Future.call_hook (fun exn -> exn) first.prg_hook local gr;
+      Lemmas.call_hook (fun exn -> exn) first.prg_hook local gr;
       List.iter progmap_remove l; kn
 
 let shrink_body c = 
@@ -816,7 +816,7 @@ let rec solve_obligation prg num tac =
           let kind = kind_of_obligation (pi2 prg.prg_kind) obl.obl_status in
             Lemmas.start_proof_univs obl.obl_name kind 
               (Universes.subst_opt_univs_constr prg.prg_subst obl.obl_type, ctx)
-              (fun (subst, ctx) -> Future.mk_hook (fun strength gr ->
+              (fun (subst, ctx) -> Lemmas.mk_hook (fun strength gr ->
 		let cst = match gr with ConstRef cst -> cst | _ -> assert false in
 		let obl =
 		  let transparent = evaluable_constant cst (Global.env ()) in
@@ -977,7 +977,7 @@ let show_term n =
 	    ++ Printer.pr_constr_env (Global.env ()) prg.prg_body)
 
 let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
-    ?(reduce=reduce) ?(hook=Future.mk_hook (fun _ _ -> ())) obls =
+    ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ -> ())) obls =
   let info = str (Id.to_string n) ++ str " has type-checked" in
   let prg = init_prog_info n term t ctx [] None [] obls implicits kind reduce hook in
   let obls,_ = prg.prg_obligations in
@@ -995,7 +995,7 @@ let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition)
 	| _ -> res)
 
 let add_mutual_definitions l ctx ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce)
-    ?(hook=Future.mk_hook (fun _ _ -> ())) notations fixkind =
+    ?(hook=Lemmas.mk_hook (fun _ _ -> ())) notations fixkind =
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
     List.iter
     (fun  (n, b, t, imps, obls) ->
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index f03e6c4468..bf186193af 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -23,7 +23,7 @@ val declare_fix_ref : (definition_kind -> Univ.universe_context -> Id.t ->
 val declare_definition_ref :
   (Id.t -> definition_kind ->
      Entries.definition_entry -> Impargs.manual_implicits
-       -> global_reference declaration_hook -> global_reference) ref
+       -> global_reference Lemmas.declaration_hook -> global_reference) ref
 
 val check_evars : env -> evar_map -> unit
 
@@ -69,7 +69,7 @@ val add_definition : Names.Id.t -> ?term:Term.constr -> Term.types ->
   ?kind:Decl_kinds.definition_kind ->
   ?tactic:unit Proofview.tactic ->
   ?reduce:(Term.constr -> Term.constr) ->
-  ?hook:unit Tacexpr.declaration_hook -> obligation_info -> progress
+  ?hook:unit Lemmas.declaration_hook -> obligation_info -> progress
 
 type notations =
     (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
@@ -85,7 +85,7 @@ val add_mutual_definitions :
   ?tactic:unit Proofview.tactic ->
   ?kind:Decl_kinds.definition_kind ->
   ?reduce:(Term.constr -> Term.constr) ->
-  ?hook:unit Tacexpr.declaration_hook ->
+  ?hook:unit Lemmas.declaration_hook ->
   notations ->
   fixpoint_kind -> unit
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 1fdf95c0f5..8e424a96ff 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -452,12 +452,12 @@ let start_proof_and_print k l hook =
   start_proof_com k l hook;
   print_subgoals ()
 
-let no_hook = Future.mk_hook (fun _ _ -> ())
+let no_hook = Lemmas.mk_hook (fun _ _ -> ())
 
 let vernac_definition_hook p = function
 | Coercion -> Class.add_coercion_hook p
 | CanonicalStructure ->
-    Future.mk_hook (fun _ -> Recordops.declare_canonical_structure)
+    Lemmas.mk_hook (fun _ -> Recordops.declare_canonical_structure)
 | SubClass -> Class.add_subclass_hook p
 | _ -> no_hook