[declare] Separate kinds from entries in constant declaration

They are clearly not at the same importance level, thus we use a named
parameter and isolate the kinds as to allow further improvements and
refactoring.

3 files changed, 17 insertions, 16 deletions

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 87910eeae7..41db9796b9 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -369,9 +369,9 @@ let generate_functional_principle (evd: Evd.evar_map ref)
         let ce = Declare.definition_entry ~univs value in
         ignore(
           Declare.declare_constant
-            name
-            (Declare.DefinitionEntry ce,
-             Decls.(IsDefinition Scheme))
+            ~name
+            ~kind:Decls.(IsDefinition Scheme)
+            (Declare.DefinitionEntry ce)
         );
         Declare.definition_message name;
         names := name :: !names
@@ -637,8 +637,9 @@ let build_scheme fas =
     (fun (princ_id,_,_) def_entry ->
        ignore
          (Declare.declare_constant
-            princ_id
-            (Declare.DefinitionEntry def_entry,Decls.(IsProof Theorem)));
+            ~name:princ_id
+            ~kind:Decls.(IsProof Theorem)
+            (Declare.DefinitionEntry def_entry));
        Declare.definition_message princ_id
     )
     fas
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index b32b27ebeb..17a96d0641 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -123,21 +123,21 @@ open DeclareDef
 
 let definition_message = Declare.definition_message
 
-let save id const ?hook uctx scope kind =
+let save name const ?hook uctx scope kind =
   let fix_exn = Future.fix_exn_of const.Proof_global.proof_entry_body in
   let r = match scope with
     | Discharge ->
-        let k = Decls.logical_kind_of_goal_kind kind in
-        let c = SectionLocalDef const in
-        let _ = declare_variable id (Lib.cwd(), c, k) in
-        VarRef id
+      let kind = Decls.logical_kind_of_goal_kind kind in
+      let c = SectionLocalDef const in
+      let _ = declare_variable ~name ~kind (Lib.cwd(), c) in
+      VarRef name
     | Global local ->
-        let k = Decls.logical_kind_of_goal_kind kind in
-        let kn = declare_constant id ~local (DefinitionEntry const, k) in
-        ConstRef kn
+      let kind = Decls.logical_kind_of_goal_kind kind in
+      let kn = declare_constant ~name ~kind ~local (DefinitionEntry const) in
+      ConstRef kn
   in
   DeclareDef.Hook.(call ?hook ~fix_exn { S.uctx; obls = []; scope; dref = r });
-  definition_message id
+  definition_message name
 
 let with_full_print f a =
   let old_implicit_args = Impargs.is_implicit_args ()
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 0398acf242..a05feed1d1 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -65,9 +65,9 @@ let find_reference sl s =
   let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in
   locate (make_qualid dp (Id.of_string s))
 
-let declare_fun f_id kind ?univs value =
+let declare_fun name kind ?univs value =
   let ce = definition_entry ?univs value (*FIXME *) in
-    ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
+  ConstRef(declare_constant ~name ~kind (DefinitionEntry ce))
 
 let defined lemma =
   Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None