Merge PR #12241: [declare] Merge DeclareDef into Declare

Reviewed-by: Matafou
Reviewed-by: SkySkimmer

2 files changed, 8 insertions, 8 deletions

diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index c53dcc7edd..608155eb71 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -218,7 +218,7 @@ let build_functional_principle (sigma : Evd.evar_map) old_princ_type sorts funs
     Declare.build_by_tactic env ~uctx ~poly:false ~typ ftac
   in
   (* uctx was ignored before *)
-  let hook = DeclareDef.Hook.make (hook new_principle_type) in
+  let hook = Declare.Hook.make (hook new_principle_type) in
   (body, typ, univs, hook, sigma)
 
 let change_property_sort evd toSort princ princName =
@@ -318,8 +318,8 @@ let generate_functional_principle (evd : Evd.evar_map ref) old_princ_type sorts
     let uctx = Evd.evar_universe_context sigma in
     let entry = Declare.definition_entry ~univs ?types body in
     let (_ : Names.GlobRef.t) =
-      DeclareDef.declare_entry ~name:new_princ_name ~hook
-        ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
+      Declare.declare_entry ~name:new_princ_name ~hook
+        ~scope:(Declare.Global Declare.ImportDefaultBehavior)
         ~kind:Decls.(IsProof Theorem)
         ~impargs:[] ~uctx entry
     in
@@ -400,7 +400,7 @@ let register_struct is_rec fixpoint_exprl =
           Pp.(str "Body of Function must be given")
     in
     ComDefinition.do_definition ~name:fname.CAst.v ~poly:false
-      ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
+      ~scope:(Declare.Global Declare.ImportDefaultBehavior)
       ~kind:Decls.Definition univs binders None body (Some rtype);
     let evd, rev_pconstants =
       List.fold_left
@@ -419,7 +419,7 @@ let register_struct is_rec fixpoint_exprl =
     (None, evd, List.rev rev_pconstants)
   | _ ->
     ComFixpoint.do_fixpoint
-      ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly:false
+      ~scope:(Declare.Global Declare.ImportDefaultBehavior) ~poly:false
       fixpoint_exprl;
     let evd, rev_pconstants =
       List.fold_left
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index ffb9a7e69b..5c82ed38bb 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1483,7 +1483,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
     let lemma = build_proof env (Evd.from_env env) start_tac end_tac in
     Lemmas.save_lemma_proved ~lemma ~opaque:opacity ~idopt:None
   in
-  let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) () in
+  let info = Lemmas.Info.make ~hook:(Declare.Hook.make hook) () in
   let lemma =
     Lemmas.start_lemma ~name:na ~poly:false (* FIXME *) ~info sigma gls_type
   in
@@ -1721,7 +1721,7 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls
   let tcc_lemma_name = add_suffix function_name "_tcc" in
   let tcc_lemma_constr = ref Undefined in
   (* let _ = Pp.msgnl (fun _ _ -> str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
-  let hook {DeclareDef.Hook.S.uctx; _} =
+  let hook {Declare.Hook.S.uctx; _} =
     let term_ref = Nametab.locate (qualid_of_ident term_id) in
     let f_ref =
       declare_f function_name Decls.(IsProof Lemma) arg_types term_ref
@@ -1767,5 +1767,5 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls
         functional_ref
         (EConstr.of_constr rec_arg_type)
         relation rec_arg_num term_id using_lemmas (List.length res_vars) evd
-        (DeclareDef.Hook.make hook))
+        (Declare.Hook.make hook))
     ()