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

10 files changed, 97 insertions, 97 deletions

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;