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

21 files changed, 180 insertions, 169 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) =
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 56f432ee1d..09d7e0278a 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -152,12 +152,12 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   let const, args = shrink_entry sign const in
   let args = List.map EConstr.of_constr args in
   let cd = Declare.DefinitionEntry { const with Proof_global.proof_entry_opaque = opaque } in
-  let decl = (cd, if opaque then Decls.(IsProof Lemma) else Decls.(IsDefinition Definition)) in
+  let kind = if opaque then Decls.(IsProof Lemma) else Decls.(IsDefinition Definition) in
   let cst () =
     (* do not compute the implicit arguments, it may be costly *)
     let () = Impargs.make_implicit_args false in
     (* ppedrot: seems legit to have abstracted subproofs as local*)
-    Declare.declare_private_constant ~local:Declare.ImportNeedQualified name decl
+    Declare.declare_private_constant ~local:Declare.ImportNeedQualified ~name ~kind cd
   in
   let cst, eff = Impargs.with_implicit_protection cst () in
   let inst = match const.Proof_global.proof_entry_universes with
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 6a7f728abc..1e87a4b6ac 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -44,8 +44,6 @@ type 'a constant_entry =
   | ParameterEntry of parameter_entry
   | PrimitiveEntry of primitive_entry
 
-type constant_declaration = Evd.side_effects constant_entry * Decls.logical_kind
-
 (* At load-time, the segment starting from the module name to the discharge *)
 (* section (if Remark or Fact) is needed to access a construction *)
 let load_constant i ((sp,kn), obj) =
@@ -235,7 +233,7 @@ let get_roles export eff =
   in
   List.map map export
 
-let define_constant ~side_effect id cd =
+let define_constant ~side_effect ~name cd =
   let open Proof_global in
   (* Logically define the constant and its subproofs, no libobject tampering *)
   let is_poly de = match de.proof_entry_universes with
@@ -270,19 +268,19 @@ let define_constant ~side_effect id cd =
     | PrimitiveEntry e ->
       [], ConstantEntry (PureEntry, Entries.PrimitiveEntry e)
   in
-  let kn, eff = Global.add_constant ~side_effect ~in_section id decl in
+  let kn, eff = Global.add_constant ~side_effect ~in_section name decl in
   kn, eff, export
 
-let declare_constant ?(local = ImportDefaultBehavior) id (cd, kind) =
-  let () = check_exists id in
-  let kn, (), export = define_constant ~side_effect:PureEntry id cd in
+let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd =
+  let () = check_exists name in
+  let kn, (), export = define_constant ~side_effect:PureEntry ~name cd in
   (* Register the libobjects attached to the constants and its subproofs *)
   let () = List.iter register_side_effect export in
   let () = register_constant kn kind local in
   kn
 
-let declare_private_constant ?role ?(local = ImportDefaultBehavior) id (cd, kind) =
-  let kn, eff, export = define_constant ~side_effect:EffectEntry id cd in
+let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind cd =
+  let kn, eff, export = define_constant ~side_effect:EffectEntry ~name cd in
   let () = assert (List.is_empty export) in
   let () = register_constant kn kind local in
   let seff_roles = match role with
@@ -294,24 +292,22 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) id (cd, kind
 
 let declare_definition
   ?(opaque=false) ?(kind=Decls.Definition) ?(local = ImportDefaultBehavior)
-  id ?types (body,univs) =
-  let cb =
-    definition_entry ?types ~univs ~opaque body
-  in
-    declare_constant ~local id
-      (DefinitionEntry cb, Decls.IsDefinition kind)
+  ~name ?types (body,univs) =
+  let cb = definition_entry ?types ~univs ~opaque body in
+  declare_constant ~local ~name ~kind:Decls.(IsDefinition kind)
+    (DefinitionEntry cb)
 
 (** Declaration of section variables and local definitions *)
 type section_variable_entry =
   | SectionLocalDef of Evd.side_effects Proof_global.proof_entry
   | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:bool }
 
-type variable_declaration = DirPath.t * section_variable_entry * Decls.logical_kind
+type variable_declaration = DirPath.t * section_variable_entry
 
 let cache_variable ((sp,_),o) =
   match o with
   | Inl ctx -> Global.push_context_set false ctx
-  | Inr (id,(path,d,kind)) ->
+  | Inr (id,(path,d),kind) ->
   (* Constr raisonne sur les noms courts *)
   if Decls.variable_exists id then
     alreadydeclared (Id.print id ++ str " already exists");
@@ -351,13 +347,13 @@ let cache_variable ((sp,_),o) =
   Decls.(add_variable_data id {path;opaque;univs;poly;kind})
 
 let discharge_variable (_,o) = match o with
-  | Inr (id,_) ->
+  | Inr (id,_,_) ->
     if Decls.variable_polymorphic id then None
     else Some (Inl (Decls.variable_context id))
   | Inl _ -> Some o
 
 type variable_obj =
-    (Univ.ContextSet.t, Id.t * variable_declaration) union
+    (Univ.ContextSet.t, Id.t * variable_declaration * Decls.logical_kind) union
 
 let inVariable : variable_obj -> obj =
   declare_object { (default_object "VARIABLE") with
@@ -366,10 +362,10 @@ let inVariable : variable_obj -> obj =
     classify_function = (fun _ -> Dispose) }
 
 (* for initial declaration *)
-let declare_variable id obj =
-  let oname = add_leaf id (inVariable (Inr (id,obj))) in
-  declare_var_implicits id;
-  Notation.declare_ref_arguments_scope Evd.empty (VarRef id);
+let declare_variable ~name ~kind obj =
+  let oname = add_leaf name (inVariable (Inr (name,obj,kind))) in
+  declare_var_implicits name;
+  Notation.declare_ref_arguments_scope Evd.empty (VarRef name);
   oname
 
 (** Declaration of inductive blocks *)
@@ -479,7 +475,7 @@ let inPrim : (Projection.Repr.t * Constant.t) -> obj =
 let declare_primitive_projection p c = Lib.add_anonymous_leaf (inPrim (p,c))
 
 let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) =
-  let id = Label.to_id label in
+  let name = Label.to_id label in
   let univs, u = match univs with
     | Monomorphic_entry _ ->
       (* Global constraints already defined through the inductive *)
@@ -490,7 +486,7 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter
   let term = Vars.subst_instance_constr u term in
   let types = Vars.subst_instance_constr u types in
   let entry = definition_entry ~types ~univs term in
-  let cst = declare_constant id (DefinitionEntry entry, Decls.(IsDefinition StructureComponent)) in
+  let cst = declare_constant ~name ~kind:Decls.(IsDefinition StructureComponent) (DefinitionEntry entry) in
   let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in
   declare_primitive_projection p cst
 
diff --git a/tactics/declare.mli b/tactics/declare.mli
index 0fc22f26c4..ae5c93db6a 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -30,15 +30,17 @@ type 'a constant_entry =
   | ParameterEntry of parameter_entry
   | PrimitiveEntry of primitive_entry
 
-type variable_declaration = DirPath.t * section_variable_entry * Decls.logical_kind
+type variable_declaration = DirPath.t * section_variable_entry
 
-val declare_variable : variable -> variable_declaration -> Libobject.object_name
+val declare_variable
+  :  name:variable
+  -> kind:Decls.logical_kind
+  -> variable_declaration
+  -> Libobject.object_name
 
 (** Declaration of global constructions
    i.e. Definition/Theorem/Axiom/Parameter/... *)
 
-type constant_declaration = Evd.side_effects constant_entry * Decls.logical_kind
-
 (* Default definition entries, transparent with no secctx or proj information *)
 val definition_entry : ?fix_exn:Future.fix_exn ->
   ?opaque:bool -> ?inline:bool -> ?types:types ->
@@ -53,16 +55,29 @@ type import_status = ImportDefaultBehavior | ImportNeedQualified
 
   internal specify if the constant has been created by the kernel or by the
   user, and in the former case, if its errors should be silent *)
-val declare_constant :
- ?local:import_status -> Id.t -> constant_declaration -> Constant.t
-
-val declare_private_constant :
-  ?role:Evd.side_effect_role -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Evd.side_effects
-
-val declare_definition :
-  ?opaque:bool -> ?kind:Decls.definition_object_kind ->
-  ?local:import_status -> Id.t -> ?types:constr ->
-  constr Entries.in_universes_entry -> Constant.t
+val declare_constant
+  :  ?local:import_status
+  -> name:Id.t
+  -> kind:Decls.logical_kind
+  -> Evd.side_effects constant_entry
+  -> Constant.t
+
+val declare_private_constant
+  :  ?role:Evd.side_effect_role
+  -> ?local:import_status
+  -> name:Id.t
+  -> kind:Decls.logical_kind
+  -> Evd.side_effects constant_entry
+  -> Constant.t * Evd.side_effects
+
+val declare_definition
+  :  ?opaque:bool
+  -> ?kind:Decls.definition_object_kind
+  -> ?local:import_status
+  -> name:Id.t
+  -> ?types:constr
+  -> constr Entries.in_universes_entry
+  -> Constant.t
 
 (** Since transparent constants' side effects are globally declared, we
  *  need that *)
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 3a3a6b94dc..90c43a1cb4 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1320,7 +1320,7 @@ let project_hint ~poly pri l2r r =
   in
   let ctx = Evd.univ_entry ~poly sigma in
   let c = EConstr.to_constr sigma c in
-  let c = Declare.declare_definition id (c,ctx) in
+  let c = Declare.declare_definition ~name:id (c,ctx) in
   let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in
     (info,false,true,PathAny, IsGlobRef (Globnames.ConstRef c))
 
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 29963bc105..e2ef05461b 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -135,7 +135,7 @@ let define internal role id c poly univs =
     proof_entry_inline_code = false;
     proof_entry_feedback = None;
   } in
-  let kn, eff = Declare.declare_private_constant ~role id (Declare.DefinitionEntry entry, Decls.(IsDefinition Scheme)) in
+  let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id (Declare.DefinitionEntry entry) in
   let () = match internal with
     | InternalTacticRequest -> ()
     | _-> Declare.definition_message id
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 2ef06d2246..2af3947dd1 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -235,7 +235,7 @@ let add_inversion_lemma ~poly name env sigma t sort dep inv_op =
   let invProof, sigma = inversion_scheme ~name ~poly env sigma t sort dep inv_op in
   let univs = Evd.univ_entry ~poly sigma in
   let entry = Declare.definition_entry ~univs invProof in
-  let _ = Declare.declare_constant name (Declare.DefinitionEntry entry, Decls.(IsProof Lemma)) in
+  let _ : Names.Constant.t = Declare.declare_constant ~name ~kind:Decls.(IsProof Lemma) (Declare.DefinitionEntry entry) in
   ()
 
 (* inv_op = Inv (derives de complete inv. lemma)
diff --git a/vernac/class.ml b/vernac/class.ml
index c0d8837c2e..f79e459f43 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -207,7 +207,7 @@ let build_id_coercion idf_opt source poly =
       user_err  (strbrk
 	"Cannot be defined as coercion (maybe a bad number of arguments).")
   in
-  let idf =
+  let name =
     match idf_opt with
       | Some idf -> idf
       | None ->
@@ -221,8 +221,8 @@ let build_id_coercion idf_opt source poly =
       (definition_entry ~types:typ_f ~univs
 	 ~inline:true (mkCast (val_f, DEFAULTcast, typ_f)))
   in
-  let decl = (constr_entry, Decls.(IsDefinition IdentityCoercion)) in
-  let kn = declare_constant idf decl in
+  let kind = Decls.(IsDefinition IdentityCoercion) in
+  let kn = declare_constant ~name ~kind constr_entry in
   ConstRef kn
 
 let check_source = function
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 01fc120af2..99a755e222 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -313,23 +313,22 @@ let instance_hook info global imps ?hook cst =
   declare_instance env sigma (Some info) (not global) cst;
   (match hook with Some h -> h cst | None -> ())
 
-let declare_instance_constant info global imps ?hook id decl poly sigma term termtype =
+let declare_instance_constant info global imps ?hook name decl poly sigma term termtype =
   (* XXX: Duplication of the declare_constant path *)
-  let kind = Decls.(IsDefinition Instance) in
   let sigma =
     let levels = Univ.LSet.union (CVars.universes_of_constr termtype)
                                  (CVars.universes_of_constr term) in
     Evd.restrict_universe_context sigma levels
   in
   let uctx = Evd.check_univ_decl ~poly sigma decl in
+  let kind = Decls.(IsDefinition Instance) in
   let entry = Declare.definition_entry ~types:termtype ~univs:uctx term in
-  let cdecl = (Declare.DefinitionEntry entry, kind) in
-  let kn = Declare.declare_constant id cdecl in
-  Declare.definition_message id;
+  let kn = Declare.declare_constant ~name ~kind (Declare.DefinitionEntry entry) in
+  Declare.definition_message name;
   Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders sigma);
   instance_hook info global imps ?hook (ConstRef kn)
 
-let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst id =
+let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst name =
   let subst = List.fold_left2
       (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst')
       [] subst (snd k.cl_context)
@@ -337,8 +336,8 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst id
   let (_, ty_constr) = instance_constructor (k,u) subst in
   let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
   let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma decl termtype in
-  let cst = Declare.declare_constant id
-      (Declare.ParameterEntry entry, Decls.(IsAssumption Logical)) in
+  let cst = Declare.declare_constant ~name
+      ~kind:Decls.(IsAssumption Logical) (Declare.ParameterEntry entry) in
   Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma);
   instance_hook pri global imps (ConstRef cst)
 
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index d7ad5133a6..60086a7861 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -42,7 +42,7 @@ let should_axiom_into_instance = let open Decls in function
     true
   | Definitional | Logical | Conjectural -> !axiom_into_instance
 
-let declare_assumption is_coe ~poly ~scope ~kind typ univs pl imps impl nl {CAst.v=ident} =
+let declare_assumption is_coe ~poly ~scope ~kind typ univs pl imps impl nl {CAst.v=name} =
 let open DeclareDef in
 match scope with
 | Discharge ->
@@ -50,10 +50,11 @@ match scope with
     | Monomorphic_entry univs -> univs
     | Polymorphic_entry (_, univs) -> Univ.ContextSet.of_context univs
   in
-  let decl = (Lib.cwd(), SectionLocalAssum {typ;univs;poly;impl}, Decls.IsAssumption kind) in
-  let _ = declare_variable ident decl in
-  let () = assumption_message ident in
-  let r = VarRef ident in
+  let kind = Decls.IsAssumption kind in
+  let decl = Lib.cwd(), SectionLocalAssum {typ; univs; poly; impl} in
+  let _ = declare_variable ~name ~kind decl in
+  let () = assumption_message name in
+  let r = VarRef name in
   let () = maybe_declare_manual_implicits true r imps in
   let env = Global.env () in
   let sigma = Evd.from_env env in
@@ -68,12 +69,13 @@ match scope with
     | DefaultInline -> Some (Flags.get_inline_level())
     | InlineAt i -> Some i
   in
-  let decl = (Declare.ParameterEntry (None,(typ,univs),inl), Decls.IsAssumption kind) in
-  let kn = declare_constant ident ~local decl in
+  let kind = Decls.IsAssumption kind in
+  let decl = Declare.ParameterEntry (None,(typ,univs),inl) in
+  let kn = declare_constant ~name ~local ~kind decl in
   let gr = ConstRef kn in
   let () = maybe_declare_manual_implicits false gr imps in
   let () = Declare.declare_univ_binders gr pl in
-  let () = assumption_message ident in
+  let () = assumption_message name in
   let env = Global.env () in
   let sigma = Evd.from_env env in
   let () = if do_instance then Classes.declare_instance env sigma None false gr in
@@ -210,7 +212,8 @@ let do_primitive id prim typopt =
                 prim_entry_content = prim;
               }
   in
-  let _kn = declare_constant id.CAst.v (PrimitiveEntry entry, Decls.IsPrimitive) in
+  let _kn : Names.Constant.t =
+    declare_constant ~name:id.CAst.v ~kind:Decls.IsPrimitive (PrimitiveEntry entry) in
   Flags.if_verbose Feedback.msg_info Pp.(Id.print id.CAst.v ++ str " is declared")
 
 let named_of_rel_context l =
@@ -268,24 +271,25 @@ let context ~poly l =
           Monomorphic_entry Univ.ContextSet.empty
         end
   in
-  let fn status (id, b, t) =
+  let fn status (name, b, t) =
     let b, t = Option.map (EConstr.to_constr sigma) b, EConstr.to_constr sigma t in
     if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
       (* Declare the universe context once *)
+      let kind = Decls.(IsAssumption Logical) in
       let decl = match b with
       | None ->
-        (Declare.ParameterEntry (None,(t,univs),None), Decls.(IsAssumption Logical))
+        Declare.ParameterEntry (None,(t,univs),None)
       | Some b ->
         let entry = Declare.definition_entry ~univs ~types:t b in
-        (Declare.DefinitionEntry entry, Decls.(IsAssumption Logical))
+        Declare.DefinitionEntry entry
       in
-      let cst = Declare.declare_constant id decl in
+      let cst = Declare.declare_constant ~name ~kind decl in
       let env = Global.env () in
       Classes.declare_instance env sigma (Some Hints.empty_hint_info) true (ConstRef cst);
       status
     else
       let test x = match x.CAst.v with
-      | Some (Name id',_) -> Id.equal id id'
+      | Some (Name id',_) -> Id.equal name id'
       | _ -> false
       in
       let impl = List.exists test impls in
@@ -294,11 +298,11 @@ let context ~poly l =
       let nstatus = match b with
       | None ->
         pi3 (declare_assumption false ~scope ~poly ~kind:Decls.Context t univs UnivNames.empty_binders [] impl
-               Declaremods.NoInline (CAst.make id))
+               Declaremods.NoInline (CAst.make name))
       | Some b ->
         let entry = Declare.definition_entry ~univs ~types:t b in
         let _gr = DeclareDef.declare_definition
-            ~name:id ~scope:DeclareDef.Discharge
+            ~name ~scope:DeclareDef.Discharge
             ~kind:Decls.Definition UnivNames.empty_binders entry [] in
         Lib.sections_are_opened () || Lib.is_modtype_strict ()
       in
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 95f8fff520..4d663d6b0e 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -212,7 +212,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
         (*FIXME poly? *)
         let ce = definition_entry ~types:ty ~univs (EConstr.to_constr sigma body) in
         (* FIXME: include locality *)
-        let c = Declare.declare_constant recname (DefinitionEntry ce, Decls.(IsDefinition Definition)) in
+        let c = Declare.declare_constant ~name:recname ~kind:Decls.(IsDefinition Definition) (DefinitionEntry ce) in
         let gr = ConstRef c in
         if Impargs.is_implicit_args () || not (List.is_empty impls) then
           Impargs.declare_manual_implicits false gr impls
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 7487c99f56..4dcb3db63b 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -48,10 +48,11 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
   let fix_exn = Future.fix_exn_of ce.Proof_global.proof_entry_body in
   let gr = match scope with
   | Discharge ->
-      let _ = declare_variable name (Lib.cwd(), SectionLocalDef ce, Decls.IsDefinition kind) in
+      let _ : Libobject.object_name =
+        declare_variable ~name ~kind:Decls.(IsDefinition kind) (Lib.cwd(), SectionLocalDef ce) in
       VarRef name
   | Global local ->
-      let kn = declare_constant name ~local (DefinitionEntry ce, Decls.IsDefinition kind) in
+      let kn = declare_constant ~name ~local ~kind:Decls.(IsDefinition kind) (DefinitionEntry ce) in
       let gr = ConstRef kn in
       let () = Declare.declare_univ_binders gr udecl in
       gr
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 0ab02862f0..a947fa2668 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -166,8 +166,9 @@ let declare_obligation prg obl body ty uctx =
     in
     (* ppedrot: seems legit to have obligations as local *)
     let constant =
-      Declare.declare_constant obl.obl_name ~local:Declare.ImportNeedQualified
-        (Declare.DefinitionEntry ce, Decls.(IsProof Property))
+      Declare.declare_constant ~name:obl.obl_name
+        ~local:Declare.ImportNeedQualified ~kind:Decls.(IsProof Property)
+        (Declare.DefinitionEntry ce)
     in
     if not opaque then
       add_hint (Locality.make_section_locality None) prg constant;
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 26499ce994..0ee15bde6e 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -99,11 +99,11 @@ let () =
 
 (* Util *)
 
-let define ~poly id sigma c t =
-  let f = declare_constant in
+let define ~poly name sigma c t =
+  let f = declare_constant ~kind:Decls.(IsDefinition Scheme) in
   let univs = Evd.univ_entry ~poly sigma in
   let open Proof_global in
-  let kn = f id
+  let kn = f ~name
     (DefinitionEntry
       { proof_entry_body = c;
         proof_entry_secctx = None;
@@ -112,9 +112,8 @@ let define ~poly id sigma c t =
         proof_entry_opaque = false;
         proof_entry_inline_code = false;
         proof_entry_feedback = None;
-      },
-      Decls.(IsDefinition Scheme)) in
-  definition_message id;
+      }) in
+  definition_message name;
   kn
 
 (* Boolean equality *)
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 2908481dea..226697a29a 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -21,8 +21,6 @@ open Declareops
 open Entries
 open Nameops
 open Globnames
-open Decls
-open Declare
 open Pretyping
 open Termops
 open Reductionops
@@ -77,7 +75,8 @@ module Info = struct
     ; kind : Decls.goal_object_kind
     }
 
-  let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Proof Lemma) () =
+  let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior)
+      ?(kind=Decls.(Proof Lemma)) () =
     { hook
     ; compute_guard = []
     ; impargs = []
@@ -120,14 +119,15 @@ let by tac pf =
 
 let retrieve_first_recthm uctx = function
   | VarRef id ->
-      (NamedDecl.get_value (Global.lookup_named id),variable_opacity id)
+    NamedDecl.get_value (Global.lookup_named id),
+    Decls.variable_opacity id
   | ConstRef cst ->
-      let cb = Global.lookup_constant cst in
-      (* we get the right order somehow but surely it could be enforced in a better way *)
-      let uctx = UState.context uctx in
-      let inst = Univ.UContext.instance uctx in
-      let map (c, _, _) = Vars.subst_instance_constr inst c in
-      (Option.map map (Global.body_of_constant_body Library.indirect_accessor cb), is_opaque cb)
+    let cb = Global.lookup_constant cst in
+    (* we get the right order somehow but surely it could be enforced in a better way *)
+    let uctx = UState.context uctx in
+    let inst = Univ.UContext.instance uctx in
+    let map (c, _, _) = Vars.subst_instance_constr inst c in
+    (Option.map map (Global.body_of_constant_body Library.indirect_accessor cb), is_opaque cb)
   | _ -> assert false
 
 let adjust_guardness_conditions const = function
@@ -252,27 +252,27 @@ let check_name_freshness locality {CAst.loc;v=id} : unit =
 let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i
     { Recthm.name; typ; impargs } =
   let t_i = norm typ in
-  let k = IsAssumption Conjectural in
+  let kind = Decls.(IsAssumption Conjectural) in
   match body with
   | None ->
     let open DeclareDef in
       (match scope with
       | Discharge ->
-          let impl = false in (* copy values from Vernacentries *)
-          let univs = match univs with
-            | Polymorphic_entry (_, univs) ->
-              (* What is going on here? *)
-              Univ.ContextSet.of_context univs
-            | Monomorphic_entry univs -> univs
-          in
-          let c = SectionLocalAssum {typ=t_i;univs;poly;impl} in
-          let _ = declare_variable name (Lib.cwd(),c,k) in
-          (VarRef name,impargs)
+        let impl = false in (* copy values from Vernacentries *)
+        let univs = match univs with
+          | Polymorphic_entry (_, univs) ->
+            (* What is going on here? *)
+            Univ.ContextSet.of_context univs
+          | Monomorphic_entry univs -> univs
+        in
+        let c = Declare.SectionLocalAssum {typ=t_i; univs; poly; impl} in
+        let _ = Declare.declare_variable ~name ~kind (Lib.cwd(),c) in
+        (VarRef name,impargs)
       | Global local ->
-          let k = IsAssumption Conjectural in
-          let decl = (ParameterEntry (None,(t_i,univs),None), k) in
-          let kn = declare_constant name ~local decl in
-          (ConstRef kn,impargs))
+        let kind = Decls.(IsAssumption Conjectural) in
+        let decl = Declare.ParameterEntry (None,(t_i,univs),None) in
+        let kn = Declare.declare_constant ~name ~local ~kind decl in
+        (ConstRef kn,impargs))
   | Some body ->
       let body = norm body in
       let rec body_i t = match Constr.kind t with
@@ -287,15 +287,13 @@ let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i
       let open DeclareDef in
       match scope with
       | Discharge ->
-          let const = definition_entry ~types:t_i ~opaque:opaq ~univs body_i in
-          let c = SectionLocalDef const in
-          let _ = declare_variable name (Lib.cwd(), c, k) in
-          (VarRef name,impargs)
+        let const = Declare.definition_entry ~types:t_i ~opaque:opaq ~univs body_i in
+        let c = Declare.SectionLocalDef const in
+        let _ = Declare.declare_variable ~name ~kind (Lib.cwd(), c) in
+        (VarRef name,impargs)
       | Global local ->
-        let const =
-          Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i
-        in
-        let kn = declare_constant name ~local (DefinitionEntry const, k) in
+        let const = Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i in
+        let kn = Declare.declare_constant ~name ~local ~kind (Declare.DefinitionEntry const) in
         (ConstRef kn,impargs)
 
 let initialize_named_context_for_proof () =
@@ -303,7 +301,7 @@ let initialize_named_context_for_proof () =
   List.fold_right
     (fun d signv ->
       let id = NamedDecl.get_id d in
-      let d = if variable_opacity id then NamedDecl.drop_body d else d in
+      let d = if Decls.variable_opacity id then NamedDecl.drop_body d else d in
       Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
 
 (* Starting a goal *)
@@ -445,10 +443,10 @@ let finish_admitted env sigma ~name ~poly ~scope pe ctx hook ~udecl impargs othe
   let open DeclareDef in
   let local = match scope with
   | Global local -> local
-  | Discharge -> warn_let_as_axiom name; ImportNeedQualified
+  | Discharge -> warn_let_as_axiom name; Declare.ImportNeedQualified
   in
-  let kn = declare_constant name ~local (ParameterEntry pe, IsAssumption Conjectural) in
-  let () = assumption_message name in
+  let kn = Declare.declare_constant ~name ~local ~kind:Decls.(IsAssumption Conjectural) (Declare.ParameterEntry pe) in
+  let () = Declare.assumption_message name in
   Declare.declare_univ_binders (ConstRef kn) (UState.universe_binders ctx);
   (* This takes care of the implicits and hook for the current constant*)
   process_recthms ?fix_exn:None ?hook env sigma ctx ~udecl ~poly ~scope:(Global local) (ConstRef kn) impargs other_thms;
@@ -496,20 +494,20 @@ let finish_proved env sigma idopt po info =
     let fix_exn = Future.fix_exn_of const.proof_entry_body in
     let () = try
       let const = adjust_guardness_conditions const compute_guard in
-      let k = Decls.logical_kind_of_goal_kind kind in
+      let kind = Decls.logical_kind_of_goal_kind kind in
       let should_suggest = const.proof_entry_opaque && Option.is_empty const.proof_entry_secctx in
       let open DeclareDef in
       let r = match scope with
         | Discharge ->
-          let c = SectionLocalDef const in
-          let _ = declare_variable name (Lib.cwd(), c, k) in
+          let c = Declare.SectionLocalDef const in
+          let _ = Declare.declare_variable ~name ~kind (Lib.cwd(), c) in
           let () = if should_suggest
             then Proof_using.suggest_variable (Global.env ()) name
           in
           VarRef name
         | Global local ->
           let kn =
-            declare_constant name ~local (DefinitionEntry const, k) in
+            Declare.declare_constant ~name ~local ~kind (Declare.DefinitionEntry const) in
           let () = if should_suggest
             then Proof_using.suggest_constant (Global.env ()) kn
           in
@@ -517,7 +515,7 @@ let finish_proved env sigma idopt po info =
           Declare.declare_univ_binders gr (UState.universe_binders universes);
           gr
       in
-      definition_message name;
+      Declare.definition_message name;
       (* This takes care of the implicits and hook for the current constant*)
       process_recthms ~fix_exn ?hook env sigma universes ~udecl ~poly ~scope r impargs other_thms
     with e when CErrors.noncritical e ->
@@ -542,8 +540,9 @@ let finish_derived ~f ~name ~idopt ~entries =
   (* The opacity of [f_def] is adjusted to be [false], as it
      must. Then [f] is declared in the global environment. *)
   let f_def = { f_def with Proof_global.proof_entry_opaque = false } in
-  let f_def = Declare.DefinitionEntry f_def , IsDefinition Definition in
-  let f_kn = Declare.declare_constant f f_def in
+  let f_kind = Decls.(IsDefinition Definition) in
+  let f_def = Declare.DefinitionEntry f_def in
+  let f_kn = Declare.declare_constant ~name:f ~kind:f_kind f_def in
   let f_kn_term = mkConst f_kn in
   (* In the type and body of the proof of [suchthat] there can be
      references to the variable [f]. It needs to be replaced by
@@ -565,17 +564,14 @@ let finish_derived ~f ~name ~idopt ~entries =
       proof_entry_body = lemma_body;
       proof_entry_type = Some lemma_type }
   in
-  let lemma_def =
-    Declare.DefinitionEntry lemma_def ,
-    Decls.(IsProof Proposition)
-  in
-  let _ : Names.Constant.t = Declare.declare_constant name lemma_def in
+  let lemma_def = Declare.DefinitionEntry lemma_def in
+  let _ : Names.Constant.t = Declare.declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in
   ()
 
 let finish_proved_equations lid kind proof_obj hook i types wits sigma0 =
 
   let obls = ref 1 in
-  let kind = match kind with
+  let kind = let open Decls in match kind with
     | DefinitionBody d -> IsDefinition d
     | Proof p -> IsProof p
   in
@@ -587,7 +583,7 @@ let finish_proved_equations lid kind proof_obj hook i types wits sigma0 =
           | None -> let n = !obls in incr obls; add_suffix i ("_obligation_" ^ string_of_int n)
         in
         let entry, args = Abstract.shrink_entry local_context entry in
-        let cst = Declare.declare_constant id (Declare.DefinitionEntry entry, kind) in
+        let cst = Declare.declare_constant ~name:id ~kind (Declare.DefinitionEntry entry) in
         let sigma, app = Evarutil.new_global sigma (ConstRef cst) in
         let sigma = Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma in
         sigma, cst) sigma0
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 92adad2299..7e615c05b0 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -688,8 +688,8 @@ let admit_prog prg =
         | None ->
             let x = subst_deps_obl obls x in
             let ctx = UState.univ_entry ~poly:false prg.prg_ctx in
-            let kn = Declare.declare_constant x.obl_name ~local:Declare.ImportNeedQualified
-              (Declare.ParameterEntry (None,(x.obl_type,ctx),None), Decls.(IsAssumption Conjectural))
+            let kn = Declare.declare_constant ~name:x.obl_name ~local:Declare.ImportNeedQualified
+              (Declare.ParameterEntry (None,(x.obl_type,ctx),None)) ~kind:Decls.(IsAssumption Conjectural)
             in
               assumption_message x.obl_name;
               obls.(i) <- { x with obl_body = Some (DefinedObl (kn, Univ.Instance.empty)) }
diff --git a/vernac/record.ml b/vernac/record.ml
index 08239eb544..7c29130383 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -351,8 +351,8 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
                     proof_entry_opaque = false;
                     proof_entry_inline_code = false;
                     proof_entry_feedback = None } in
-                  let k = (Declare.DefinitionEntry entry,Decls.IsDefinition kind) in
-                  let kn = declare_constant fid k in
+                  let kind = Decls.IsDefinition kind in
+                  let kn = declare_constant ~name:fid ~kind (Declare.DefinitionEntry entry) in
 		  let constr_fip =
 		    let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
 		      applist (mkConstU (kn,u),proj_args) 
@@ -496,8 +496,8 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity
       let class_type = it_mkProd_or_LetIn arity params in
       let class_entry = 
         Declare.definition_entry ~types:class_type ~univs class_body in
-      let cst = Declare.declare_constant id
-        (DefinitionEntry class_entry, Decls.(IsDefinition Definition))
+      let cst = Declare.declare_constant ~name:id
+        (DefinitionEntry class_entry) ~kind:Decls.(IsDefinition Definition)
       in
       let inst, univs = match univs with
         | Polymorphic_entry (_, uctx) -> Univ.UContext.instance uctx, univs
@@ -511,8 +511,8 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity
       let proj_body =
         it_mkLambda_or_LetIn (mkLambda (binder, inst_type, mkRel 1)) params in
       let proj_entry = Declare.definition_entry ~types:proj_type ~univs proj_body in
-      let proj_cst = Declare.declare_constant proj_name
-        (DefinitionEntry proj_entry, Decls.(IsDefinition Definition))
+      let proj_cst = Declare.declare_constant ~name:proj_name
+        (DefinitionEntry proj_entry) ~kind:Decls.(IsDefinition Definition)
       in
       let cref = ConstRef cst in
       Impargs.declare_manual_implicits false cref paramimpls;