[proof] Move declaration hooks to DeclareDef.

This way both `Lemmas` and `DeclareObl` can depend on it, removing one
more difficulty on the unification of terminators.

20 files changed, 93 insertions, 81 deletions

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 8af5dc818b..08acb754f7 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -307,7 +307,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
   in
   let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd (EConstr.of_constr new_principle_type) in
   evd := sigma;
-  let hook = Lemmas.mk_hook (hook new_principle_type) in
+  let hook = DeclareDef.Hook.make (hook new_principle_type) in
   let lemma =
     Lemmas.start_lemma
       new_princ_name
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 7683ce1757..732a0d818f 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -137,7 +137,7 @@ let save id const ?hook uctx (locality,_,kind) =
         let kn = declare_constant id ~local (DefinitionEntry const, k) in
         ConstRef kn
   in
-  Lemmas.call_hook ?hook ~fix_exn uctx [] locality r;
+  DeclareDef.Hook.call ?hook ~fix_exn uctx [] locality r;
   definition_message id
 
 let with_full_print f a =
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 4078c34331..8dd990775b 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -45,7 +45,7 @@ val jmeq_refl : unit -> EConstr.constr
 val save
   :  Id.t
   -> Evd.side_effects Entries.definition_entry
-  -> ?hook:Lemmas.declaration_hook
+  -> ?hook:DeclareDef.Hook.t
   -> UState.t
   -> Decl_kinds.goal_kind
   -> unit
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 2b5c0a01db..8169ff459f 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1371,7 +1371,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
   let lemma = Lemmas.start_lemma
     na
     Decl_kinds.(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma)
-    sigma gls_type ~hook:(Lemmas.mk_hook hook) in
+    sigma gls_type ~hook:(DeclareDef.Hook.make hook) in
   let lemma = if Indfun_common.is_strict_tcc  ()
   then
     fst @@ Lemmas.by (Proofview.V82.tactic (tclIDTAC)) lemma
@@ -1592,5 +1592,5 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type
         term_id
         using_lemmas
         (List.length res_vars)
-        evd (Lemmas.mk_hook hook))
+        evd (DeclareDef.Hook.make hook))
     ()
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 2da6584aba..2bab55ef74 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -2006,7 +2006,7 @@ let add_morphism_interactive atts m n : Lemmas.t =
       declare_projection n instance_id (ConstRef cst)
     | _ -> assert false
   in
-  let hook = Lemmas.mk_hook hook in
+  let hook = DeclareDef.Hook.make hook in
   Flags.silently
     (fun () ->
        let lemma = Lemmas.start_lemma ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in
diff --git a/vernac/class.ml b/vernac/class.ml
index 58cef5db4f..eed7107b39 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -366,7 +366,7 @@ let add_coercion_hook poly _uctx _trans local ref =
   let msg = Nametab.pr_global_env Id.Set.empty ref ++ str " is now a coercion" in
   Flags.if_verbose Feedback.msg_info msg
 
-let add_coercion_hook poly = Lemmas.mk_hook (add_coercion_hook poly)
+let add_coercion_hook poly = DeclareDef.Hook.make (add_coercion_hook poly)
 
 let add_subclass_hook poly _uctx _trans local ref =
   let stre = match local with
@@ -377,4 +377,4 @@ let add_subclass_hook poly _uctx _trans local ref =
   let cl = class_of_global ref in
   try_add_new_coercion_subclass cl ~local:stre poly
 
-let add_subclass_hook poly = Lemmas.mk_hook (add_subclass_hook poly)
+let add_subclass_hook poly = DeclareDef.Hook.make (add_subclass_hook poly)
diff --git a/vernac/class.mli b/vernac/class.mli
index 80d6d4383c..85266739ad 100644
--- a/vernac/class.mli
+++ b/vernac/class.mli
@@ -42,8 +42,8 @@ val try_add_new_coercion_with_source : GlobRef.t -> 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 -> Lemmas.declaration_hook
+val add_coercion_hook : Decl_kinds.polymorphic -> DeclareDef.Hook.t
 
-val add_subclass_hook : Decl_kinds.polymorphic -> Lemmas.declaration_hook
+val add_subclass_hook : Decl_kinds.polymorphic -> DeclareDef.Hook.t
 
 val class_of_global : GlobRef.t -> cl_typ
diff --git a/vernac/classes.ml b/vernac/classes.ml
index bd5a211f1d..74903d196f 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -364,7 +364,7 @@ let declare_instance_program env sigma ~global ~poly id pri imps decl term termt
       in obls, Some constr, typ
     | None -> [||], None, termtype
   in
-  let hook = Lemmas.mk_hook hook in
+  let hook = DeclareDef.Hook.make hook in
   let ctx = Evd.evar_universe_context sigma in
   ignore(Obligations.add_definition id ?term:constr
            ~univdecl:decl typ ctx ~kind:(Global ImportDefaultBehavior,poly,Instance) ~hook obls)
@@ -379,7 +379,7 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps decl ids te
   let sigma = Evd.reset_future_goals sigma in
   let kind = Decl_kinds.(Global ImportDefaultBehavior, poly, DefinitionBody Instance) in
   let lemma = Lemmas.start_lemma id ~pl:decl kind sigma (EConstr.of_constr termtype)
-      ~hook:(Lemmas.mk_hook
+      ~hook:(DeclareDef.Hook.make
                (fun _ _ _ -> instance_hook pri global imps ?hook)) in
   (* spiwack: I don't know what to do with the status here. *)
   let lemma =
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 0d9df47ee8..cf309d6bbd 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -18,7 +18,7 @@ open Constrexpr
 
 val do_definition
   : program_mode:bool
-  -> ?hook:Lemmas.declaration_hook
+  -> ?hook:DeclareDef.Hook.t
   -> Id.t
   -> definition_kind
   -> universe_decl_expr option
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 6296347fd0..3bb9b0f6a1 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -229,7 +229,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
       in hook, recname, typ
   in
   (* XXX: Capturing sigma here... bad bad *)
-  let hook = Lemmas.mk_hook (hook sigma) in
+  let hook = DeclareDef.Hook.make (hook sigma) in
   Obligations.check_evars env sigma;
   let evars, _, evars_def, evars_typ =
     Obligations.eterm_obligations env recname sigma 0 def typ
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 652dbf0858..f80884c124 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -14,6 +14,29 @@ open Entries
 open Globnames
 open Impargs
 
+(* Hooks naturally belong here as they apply to both definitions and lemmas *)
+module Hook = struct
+  module S = struct
+    type t = UState.t
+      -> (Names.Id.t * Constr.t) list
+      -> Decl_kinds.locality
+      -> Names.GlobRef.t
+      -> unit
+  end
+
+  type t = S.t CEphemeron.key
+
+  let make hook = CEphemeron.create hook
+
+  let call ?hook ?fix_exn uctx trans l c =
+    try Option.iter (fun hook -> CEphemeron.get hook uctx trans l c) hook
+    with e when CErrors.noncritical e ->
+      let e = CErrors.push e in
+      let e = Option.cata (fun fix -> fix e) e fix_exn in
+      Util.iraise e
+end
+
+(* Locality stuff *)
 let declare_definition ident (local, p, k) ?hook_data ce pl imps =
   let fix_exn = Future.fix_exn_of ce.const_entry_body in
   let gr = match local with
@@ -32,7 +55,7 @@ let declare_definition ident (local, p, k) ?hook_data ce pl imps =
     match hook_data with
     | None -> ()
     | Some (hook, uctx, extra_defs) ->
-      Lemmas.call_hook ~fix_exn ~hook uctx extra_defs local gr
+      Hook.call ~fix_exn ~hook uctx extra_defs local gr
   end;
   gr
 
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 909aa41a30..5b656a2f5a 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -11,10 +11,38 @@
 open Names
 open Decl_kinds
 
+(** Declaration hooks *)
+module Hook : sig
+  type t
+
+  (** Hooks allow users of the API to perform arbitrary actions at
+     proof/definition saving time. For example, to register a constant
+     as a Coercion, perform some cleanup, update the search database,
+     etc...  *)
+  module S : sig
+    (** [S.t] passes to the client: *)
+    type t
+      =  UState.t
+      (** [ustate]: universe constraints obtained when the term was closed *)
+      -> (Id.t * Constr.t) list
+      (** [(n1,t1),...(nm,tm)]: association list between obligation
+          name and the corresponding defined term (might be a constant,
+          but also an arbitrary term in the Expand case of obligations) *)
+      -> Decl_kinds.locality
+      (**  [locality]: Locality of the original declaration *)
+      -> GlobRef.t
+      (** [ref]: identifier of the origianl declaration *)
+      -> unit
+  end
+
+  val make : S.t -> t
+  val call : ?hook:t -> ?fix_exn:Future.fix_exn -> S.t
+end
+
 val declare_definition
   : Id.t
   -> definition_kind
-  -> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list)
+  -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
   -> Evd.side_effects Entries.definition_entry
   -> UnivNames.universe_binders
   -> Impargs.manual_implicits
@@ -22,7 +50,7 @@ val declare_definition
 
 val declare_fix
   : ?opaque:bool
-  -> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list)
+  -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
   -> definition_kind
   -> UnivNames.universe_binders
   -> Entries.universes_entry
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 2afd056950..b269f69ece 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -50,7 +50,7 @@ type program_info =
   ; prg_notations : notations
   ; prg_kind : definition_kind
   ; prg_reduce : constr -> constr
-  ; prg_hook : Lemmas.declaration_hook option
+  ; prg_hook : DeclareDef.Hook.t option
   ; prg_opaque : bool
   ; prg_sign : named_context_val }
 
@@ -451,7 +451,7 @@ let declare_mutual_definition l =
     first.prg_notations;
   Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
   let gr = List.hd kns in
-  Lemmas.call_hook ?hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr;
+  DeclareDef.Hook.call ?hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr;
   List.iter progmap_remove l;
   gr
 
diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli
index ab305da3af..5d02639245 100644
--- a/vernac/declareObl.mli
+++ b/vernac/declareObl.mli
@@ -44,7 +44,7 @@ type program_info =
   ; prg_notations : notations
   ; prg_kind : Decl_kinds.definition_kind
   ; prg_reduce : constr -> constr
-  ; prg_hook : Lemmas.declaration_hook option
+  ; prg_hook : DeclareDef.Hook.t option
   ; prg_opaque : bool
   ; prg_sign : Environ.named_context_val }
 
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 0ca273a02d..98c7c0d077 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -33,18 +33,6 @@ open Impargs
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
-type hook_type = UState.t -> (Id.t * Constr.t) list -> Decl_kinds.locality -> GlobRef.t -> unit
-type declaration_hook = hook_type CEphemeron.key
-
-let mk_hook hook = CEphemeron.create hook
-
-let call_hook ?hook ?fix_exn uctx trans l c =
-  try Option.iter (fun hook -> CEphemeron.get hook uctx trans l c) hook
-  with e when CErrors.noncritical e ->
-    let e = CErrors.push e in
-    let e = Option.cata (fun fix -> fix e) e fix_exn in
-    iraise e
-
 (* Support for terminators and proofs with an associated constant
    [that can be saved] *)
 
@@ -56,13 +44,13 @@ type proof_ending =
       Decl_kinds.goal_kind *
       Entries.parameter_entry *
       UState.t *
-      declaration_hook option
+      DeclareDef.Hook.t option
 
   | Proved of
       Proof_global.opacity_flag *
       lident option *
       Proof_global.proof_object *
-      declaration_hook option *
+      DeclareDef.Hook.t option *
       lemma_possible_guards
 
 type proof_terminator = (proof_ending -> unit) CEphemeron.key
@@ -71,7 +59,7 @@ type proof_terminator = (proof_ending -> unit) CEphemeron.key
 type t =
   { proof : Proof_global.t
   ; terminator : proof_terminator
-  ; hook : declaration_hook option
+  ; hook : DeclareDef.Hook.t option
   ; compute_guard : lemma_possible_guards
   }
 
@@ -247,7 +235,7 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook universes
           gr
     in
     definition_message id;
-    call_hook ~fix_exn ?hook universes [] locality r
+    DeclareDef.Hook.call ~fix_exn ?hook universes [] locality r
   with e when CErrors.noncritical e ->
     let e = CErrors.push e in
     iraise (fix_exn e)
@@ -326,7 +314,7 @@ let admit ?hook ctx (id,k,e) pl () =
   let kn = declare_constant id ~local (ParameterEntry e, IsAssumption Conjectural) in
   let () = assumption_message id in
   Declare.declare_univ_binders (ConstRef kn) pl;
-  call_hook ?hook ctx [] (Global local) (ConstRef kn)
+  DeclareDef.Hook.call ?hook ctx [] (Global local) (ConstRef kn)
 
 (* Starting a goal *)
 
@@ -448,8 +436,8 @@ let start_lemma_with_initialization ?hook kind sigma decl recguard thms snl =
         let thms_data = (ref,imps)::other_thms_data in
         List.iter (fun (ref,imps) ->
 	  maybe_declare_manual_implicits false ref imps;
-          call_hook ?hook ctx [] strength ref) thms_data in
-      let hook = mk_hook hook in
+          DeclareDef.Hook.call ?hook ctx [] strength ref) thms_data in
+      let hook = DeclareDef.Hook.make hook in
       let lemma = start_lemma id ~pl:decl kind sigma t ~hook ~compute_guard:guard in
       let lemma = pf_map (Proof_global.map_proof (fun p ->
           match init_tac with
@@ -549,7 +537,7 @@ let save_lemma_admitted ?proof ~(lemma : t) =
   in
   CEphemeron.get lemma.terminator pe
 
-type proof_info = proof_terminator * declaration_hook option * lemma_possible_guards
+type proof_info = proof_terminator * DeclareDef.Hook.t option * lemma_possible_guards
 
 let default_info = standard_proof_terminator, None, []
 
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 3efaac672a..961c1e41ef 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -11,33 +11,6 @@
 open Names
 open Decl_kinds
 
-(* Declaration hooks *)
-type declaration_hook
-
-(* Hooks allow users of the API to perform arbitrary actions at
- * proof/definition saving time. For example, to register a constant
- * as a Coercion, perform some cleanup, update the search database,
- * etc...
- *
- * Here, we use an extended hook type suitable for obligations /
- * equations.
- *)
-(** [hook_type] passes to the client:
-    - [ustate]: universe constraints obtained when the term was closed
-    - [(n1,t1),...(nm,tm)]: association list between obligation
-        name and the corresponding defined term (might be a constant,
-        but also an arbitrary term in the Expand case of obligations)
-    - [locality]: Locality of the original declaration
-    - [ref]: identifier of the origianl declaration
- *)
-type hook_type = UState.t -> (Id.t * Constr.t) list -> Decl_kinds.locality -> GlobRef.t -> unit
-
-val mk_hook : hook_type -> declaration_hook
-val call_hook
-  :  ?hook:declaration_hook
-  -> ?fix_exn:Future.fix_exn
-  -> hook_type
-
 (* Proofs that define a constant + terminators *)
 type t
 type proof_terminator
@@ -83,7 +56,7 @@ val start_lemma
   -> ?terminator:proof_terminator
   -> ?sign:Environ.named_context_val
   -> ?compute_guard:lemma_possible_guards
-  -> ?hook:declaration_hook
+  -> ?hook:DeclareDef.Hook.t
   -> EConstr.types
   -> t
 
@@ -94,18 +67,18 @@ val start_dependent_lemma
   -> ?terminator:proof_terminator
   -> ?sign:Environ.named_context_val
   -> ?compute_guard:lemma_possible_guards
-  -> ?hook:declaration_hook
+  -> ?hook:DeclareDef.Hook.t
   -> Proofview.telescope
   -> t
 
 val start_lemma_com
   :  program_mode:bool
   -> ?inference_hook:Pretyping.inference_hook
-  -> ?hook:declaration_hook -> goal_kind -> Vernacexpr.proof_expr list
+  -> ?hook:DeclareDef.Hook.t -> goal_kind -> Vernacexpr.proof_expr list
   -> t
 
 val start_lemma_with_initialization
-  :  ?hook:declaration_hook
+  :  ?hook:DeclareDef.Hook.t
   -> goal_kind -> Evd.evar_map -> UState.universe_decl
   -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option
   -> (Id.t (* name of thm *) *
@@ -146,12 +119,12 @@ type proof_ending =
       Decl_kinds.goal_kind *
       Entries.parameter_entry *
       UState.t *
-      declaration_hook option
+      DeclareDef.Hook.t option
   | Proved of
       Proof_global.opacity_flag *
       lident option *
       Proof_global.proof_object *
-      declaration_hook option *
+      DeclareDef.Hook.t option *
       lemma_possible_guards
 
 (** This stuff is internal and will be removed in the future.  *)
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index b6f2c47f98..9a34bda423 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -493,7 +493,7 @@ let rec solve_obligation prg num tac =
   let auto n tac oblset = auto_solve_obligations n ~oblset tac in
   let terminator = Lemmas.Internal.make_terminator
       (obligation_terminator prg.prg_name num auto) in
-  let hook = Lemmas.mk_hook (obligation_hook prg obl num auto) in
+  let hook = DeclareDef.Hook.make (obligation_hook prg obl num auto) in
   let lemma = Lemmas.start_lemma ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~hook in
   let lemma = fst @@ Lemmas.by !default_tactic lemma in
   let lemma = Option.cata (fun tac -> Lemmas.set_endline_tactic tac lemma) lemma tac in
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 5e6339e9b9..87da73c534 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -51,7 +51,7 @@ val add_definition
   -> ?kind:Decl_kinds.definition_kind
   -> ?tactic:unit Proofview.tactic
   -> ?reduce:(constr -> constr)
-  -> ?hook:Lemmas.declaration_hook
+  -> ?hook:DeclareDef.Hook.t
   -> ?opaque:bool
   -> obligation_info
   -> DeclareObl.progress
@@ -63,7 +63,7 @@ val add_mutual_definitions :
   ?tactic:unit Proofview.tactic ->
   ?kind:Decl_kinds.definition_kind ->
   ?reduce:(constr -> constr) ->
-  ?hook:Lemmas.declaration_hook -> ?opaque:bool ->
+  ?hook:DeclareDef.Hook.t -> ?opaque:bool ->
   DeclareObl.notations ->
   DeclareObl.fixpoint_kind -> unit
 
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index f58af33f08..0749314301 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -11,16 +11,16 @@ Egramml
 Vernacextend
 Ppvernac
 Proof_using
+Egramcoq
+Metasyntax
+DeclareDef
 Lemmas
+DeclareObl
 Canonical
 Class
-Egramcoq
-Metasyntax
 Auto_ind_decl
 Search
 Indschemes
-DeclareDef
-DeclareObl
 Obligations
 ComDefinition
 Classes
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 112c4b6451..bf57866d95 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -588,7 +588,7 @@ let vernac_definition_hook p = function
 | Coercion ->
   Some (Class.add_coercion_hook p)
 | CanonicalStructure ->
-  Some (Lemmas.mk_hook (fun _ _ _ -> Canonical.declare_canonical_structure))
+  Some (DeclareDef.Hook.make (fun _ _ _ -> Canonical.declare_canonical_structure))
 | SubClass ->
   Some (Class.add_subclass_hook p)
 | _ -> None