[declare] Generalize kind type on declareDef

This is useful to remove some duplicate bits in other declare files.

6 files changed, 9 insertions, 6 deletions

diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index 9dd4700db5..307214089f 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -9,4 +9,4 @@ let edeclare ?hook ~name ~poly ~scope ~kind ~opaque sigma udecl body tyopt imps
 let declare_definition ~poly name sigma body =
   let udecl = UState.default_univ_decl in
   edeclare ~name ~poly ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
-    ~kind:Decls.Definition ~opaque:false sigma udecl body None []
+    ~kind:Decls.(IsDefinition Definition) ~opaque:false sigma udecl body None []
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index f9b73a59eb..a0b0dcf4c8 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -217,7 +217,7 @@ let context_insection sigma ~poly ctx =
         in
         let entry = Declare.definition_entry ~univs ~types:t b in
         let _ : GlobRef.t = DeclareDef.declare_definition ~name ~scope:DeclareDef.Discharge
-            ~kind:Decls.Definition UnivNames.empty_binders entry []
+            ~kind:Decls.(IsDefinition Definition) UnivNames.empty_binders entry []
         in
         ()
     in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 9745358ba2..5b3f15a08c 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -104,4 +104,5 @@ let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind univdecl bl red_o
     let ce = check_definition ~program_mode def in
     let uctx = Evd.evar_universe_context evd in
     let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
+    let kind = Decls.IsDefinition kind in
     ignore(DeclareDef.declare_definition ~name ~scope ~kind ?hook_data (Evd.universe_binders evd) ce imps)
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 1926faaf0e..67733c95a1 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -48,11 +48,11 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
   let gr = match scope with
   | Discharge ->
       let () =
-        declare_variable ~name ~kind:Decls.(IsDefinition kind) (SectionLocalDef ce)
+        declare_variable ~name ~kind (SectionLocalDef ce)
       in
       Names.GlobRef.VarRef name
   | Global local ->
-      let kn = declare_constant ~name ~local ~kind:Decls.(IsDefinition kind) (DefinitionEntry ce) in
+      let kn = declare_constant ~name ~local ~kind (DefinitionEntry ce) in
       let gr = Names.GlobRef.ConstRef kn in
       let () = Declare.declare_univ_binders gr udecl in
       gr
@@ -69,6 +69,7 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
 
 let declare_fix ?(opaque = false) ?hook_data ~name ~scope ~kind udecl univs ((def,_),eff) t imps =
   let ce = definition_entry ~opaque ~types:t ~univs ~eff def in
+  let kind = Decls.IsDefinition kind in
   declare_definition ~name ~scope ~kind ?hook_data udecl ce imps
 
 let check_definition_evars ~allow_evars sigma =
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 54a0c9a7e8..d6001f5970 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -42,7 +42,7 @@ end
 val declare_definition
   :  name:Id.t
   -> scope:locality
-  -> kind:Decls.definition_object_kind
+  -> kind:Decls.logical_kind
   -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
   -> UnivNames.universe_binders
   -> Evd.side_effects Declare.proof_entry
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 8fd6bc7eab..2c56f707f1 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -351,7 +351,8 @@ let declare_definition prg =
   let ubinders = UState.universe_binders uctx in
   let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in
   DeclareDef.declare_definition
-    ~name:prg.prg_name ~scope:prg.prg_scope ubinders ~kind:prg.prg_kind ce
+    ~name:prg.prg_name ~scope:prg.prg_scope ubinders
+    ~kind:Decls.(IsDefinition prg.prg_kind) ce
     prg.prg_implicits ?hook_data
 
 let rec lam_index n t acc =