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

1 files changed, 8 insertions, 9 deletions

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));