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

Reviewed-by: Matafou
Reviewed-by: SkySkimmer

1 files changed, 2 insertions, 2 deletions

diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 66d5a4f7f5..95f3955309 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -117,7 +117,7 @@ let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
   in
   let kind = Decls.IsDefinition kind in
   let _ : Names.GlobRef.t =
-    DeclareDef.declare_definition ~name ~scope ~kind ?hook ~impargs
+    Declare.declare_definition ~name ~scope ~kind ?hook ~impargs
       ~opaque:false ~poly evd ~udecl ~types ~body
   in ()
 
@@ -126,7 +126,7 @@ let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c c
   let (body, types), evd, udecl, impargs =
     interp_definition ~program_mode udecl bl ~poly red_option c ctypopt
   in
-  let term, ty, uctx, obls = DeclareDef.prepare_obligation ~name ~poly ~body ~types ~udecl evd in
+  let term, ty, uctx, obls = Declare.prepare_obligation ~name ~poly ~body ~types ~udecl evd in
   let _ : DeclareObl.progress =
     Obligations.add_definition
       ~name ~term ty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls