More precise type for universe entries.

We use an algebraic type instead of a pair of a boolean and the corresponding
data. For now, this is isomorphic, but this allows later change in the structure.

1 files changed, 6 insertions, 2 deletions

diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 3d97a767c..6ea8bc7f2 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -109,13 +109,17 @@ let _ =
 
 let define id internal ctx c t =
   let f = declare_constant ~internal in
+  let _, univs = Evd.universe_context ctx in
+  let univs =
+    if Flags.is_universe_polymorphism () then Polymorphic_const_entry univs
+    else Monomorphic_const_entry univs
+  in
   let kn = f id
     (DefinitionEntry
       { const_entry_body = c;
         const_entry_secctx = None;
         const_entry_type = t;
-	const_entry_polymorphic = Flags.is_universe_polymorphism ();
-	const_entry_universes = snd (Evd.universe_context ctx);
+	const_entry_universes = univs;
         const_entry_opaque = false;
         const_entry_inline_code = false;
         const_entry_feedback = None;