From 0bc7e7405553dc63d9693e85c3ce1485b5e8fe23 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 21 Jun 2019 20:56:33 +0200
Subject: [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.
---
 plugins/setoid_ring/newring.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/setoid_ring')

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) =
-- 
cgit v1.2.3