[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.

5 files changed, 28 insertions, 28 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
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 22ad75b784..bef0dcc189 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1898,11 +1898,11 @@ let declare_projection n instance_id r =
   let univs = Evd.univ_entry ~poly sigma in
   let typ = EConstr.to_constr sigma typ in
   let term = EConstr.to_constr sigma term in
-  let cst = 
-    Declare.definition_entry ~types:typ ~univs term
-  in
-    ignore(Declare.declare_constant n
-           (Declare.DefinitionEntry cst, Decls.(IsDefinition Definition)))
+  let cst = Declare.definition_entry ~types:typ ~univs term in
+  let _ : Constant.t =
+    Declare.declare_constant ~name:n ~kind:Decls.(IsDefinition Definition)
+      (Declare.DefinitionEntry cst)
+  in ()
 
 let build_morphism_signature env sigma m =
   let m,ctx = Constrintern.interp_constr env sigma m in
@@ -1978,10 +1978,9 @@ let add_morphism_as_parameter atts m n : unit =
   let evd = Evd.from_env env in
   let uctx, instance = build_morphism_signature env evd m in
   let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in
-  let cst = Declare.declare_constant instance_id
-      (Declare.ParameterEntry
-         (None,(instance,uctx),None),
-       Decls.(IsAssumption Logical))
+  let cst = Declare.declare_constant ~name:instance_id
+      ~kind:Decls.(IsAssumption Logical)
+      (Declare.ParameterEntry (None,(instance,uctx),None))
   in
   Classes.add_instance (Classes.mk_instance
                   (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst));
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 3d6bfda0b2..9973f2ec1d 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -155,9 +155,9 @@ let decl_constant na univs c =
   let () = Declare.declare_universe_context ~poly:false univs in
   let types = (Typeops.infer (Global.env ()) c).uj_type in
   let univs = Monomorphic_entry Univ.ContextSet.empty in
-  mkConst(declare_constant (Id.of_string na) 
-            (DefinitionEntry (definition_entry ~opaque:true ~types ~univs c),
-             Decls.(IsProof Lemma)))
+  mkConst(declare_constant ~name:(Id.of_string na)
+            ~kind:Decls.(IsProof Lemma)
+            (DefinitionEntry (definition_entry ~opaque:true ~types ~univs c)))
 
 (* Calling a global tactic *)
 let ltac_call tac (args:glob_tactic_arg list) =