[vernac] Unify declaration hooks.

Supersedes #8718.

5 files changed, 18 insertions, 10 deletions

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 25a7675113..ca09cad1f3 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -353,7 +353,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
   in
   let names = ref [new_princ_name] in
   let hook =
-    fun  new_principle_type _ _  -> 
+    fun new_principle_type _ _ _ _  ->
     if Option.is_empty sorts
     then
       (*     let id_of_f = Label.to_id (con_label f) in *)
@@ -385,7 +385,8 @@ let generate_functional_principle (evd: Evd.evar_map ref)
   (* Pr  1278 :
      Don't forget to close the goal if an error is raised !!!!
   *)
-  save false new_princ_name entry g_kind ~hook
+  let uctx = Evd.evar_universe_context sigma in
+  save false new_princ_name entry ~hook uctx g_kind
   with e when CErrors.noncritical e ->
     begin
       begin
@@ -539,7 +540,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
 	this_block_funs
 	0
 	(prove_princ_for_struct evd false 0 (Array.of_list (List.map fst funs)))
-	(fun _ _ _ -> ())
+        (fun _ _ _ _ _ -> ())
     with e when CErrors.noncritical e ->
        begin
 	 begin
@@ -614,7 +615,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
 		 this_block_funs
 		 !i
 		 (prove_princ_for_struct evd false !i (Array.of_list (List.map fst funs)))
-		 (fun _ _ _ -> ())
+                 (fun _ _ _ _ _ -> ())
 	     in
 	     const
 	 with Found_type i ->
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index f9938c0356..cba3cc3d42 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -129,7 +129,7 @@ let get_locality = function
 | Local -> true
 | Global -> false
 
-let save with_clean id const ?hook (locality,_,kind) =
+let save with_clean id const ?hook uctx (locality,_,kind) =
   let fix_exn = Future.fix_exn_of const.const_entry_body in
   let l,r = match locality with
     | Discharge when Lib.sections_are_opened () ->
@@ -144,7 +144,7 @@ let save with_clean id const ?hook (locality,_,kind) =
 	(locality, ConstRef kn)
   in
   if with_clean then Proof_global.discard_current ();
-  Lemmas.call_hook ?hook ~fix_exn l r;
+  Lemmas.call_hook ?hook ~fix_exn uctx [] l 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 9584649cff..1e0b95df34 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -42,7 +42,14 @@ val const_of_id: Id.t ->  GlobRef.t(* constantyes *)
 val jmeq : unit -> EConstr.constr
 val jmeq_refl : unit -> EConstr.constr
 
-val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> ?hook:Lemmas.declaration_hook -> Decl_kinds.goal_kind -> unit
+val save
+  :  bool
+  -> Id.t
+  -> Safe_typing.private_constants Entries.definition_entry
+  -> ?hook:Lemmas.declaration_hook
+  -> UState.t
+  -> Decl_kinds.goal_kind
+  -> unit
 
 (* [with_full_print f a] applies [f] to [a] in full printing environment.
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index a8517e9ab1..8746c37309 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1310,7 +1310,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
   let na = next_global_ident_away name Id.Set.empty in
   if Termops.occur_existential sigma gls_type then
     CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials");
-  let hook _ _ =
+  let hook _ _ _ _ =
     let opacity =
       let na_ref = qualid_of_ident na in
       let na_global = Smartlocate.global_with_alias na_ref in
@@ -1560,7 +1560,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let tcc_lemma_name = add_suffix function_name "_tcc" in
   let tcc_lemma_constr = ref Undefined in
   (* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
-  let hook _ _ = 
+  let hook _ _ _ _ =
     let term_ref = Nametab.locate (qualid_of_ident term_id) in
     let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in
     let _ = Extraction_plugin.Table.extraction_inline true [qualid_of_ident term_id] in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 7da4464e59..2d833a2cde 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1989,7 +1989,7 @@ let add_morphism_infer atts m n =
 	Decl_kinds.DefinitionBody Decl_kinds.Instance 
       in
       let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
-      let hook _ = function
+      let hook _ _ _ = function
 	| Globnames.ConstRef cst ->
 	  add_instance (Typeclasses.new_instance 
 			  (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info