Separate variance and universe fields in inductives.

I think the usage looks cleaner this way.

4 files changed, 5 insertions, 5 deletions

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 12b68e208c..25a7675113 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -364,7 +364,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
         let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
         let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in
         (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
-        let univs = Evd.const_univ_entry ~poly:false evd' in
+        let univs = Evd.univ_entry ~poly:false evd' in
         let ce = Declare.definition_entry ~univs value in
         ignore(
 	  Declare.declare_constant
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 0c97f9f373..a8517e9ab1 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1547,7 +1547,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let functional_id =  add_suffix function_name "_F" in
   let term_id = add_suffix function_name "_terminate" in
   let functional_ref =
-    let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evd) in
+    let univs = Evd.univ_entry ~poly:false evd in
     declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res
   in
   (* Refresh the global universes, now including those of _F *)
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 2055b25ff4..7da4464e59 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1889,7 +1889,7 @@ let declare_projection n instance_id r =
     in it_mkProd_or_LetIn ccl ctx
   in
   let typ = it_mkProd_or_LetIn typ ctx in
-  let univs = Evd.const_univ_entry ~poly sigma in
+  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 = 
@@ -1975,7 +1975,7 @@ let add_morphism_infer atts m n =
   let evd = Evd.from_env env in
   let uctx, instance = build_morphism_signature env evd m in
     if Lib.is_modtype () then
-      let uctx = UState.const_univ_entry ~poly:atts.polymorphic uctx in
+      let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in
       let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
 				(Entries.ParameterEntry 
                                  (None,(instance,uctx),None),
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 65201d922f..3f69701bd3 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -153,7 +153,7 @@ let decl_constant na univs c =
   let open Constr in
   let vars = CVars.universes_of_constr c in
   let univs = UState.restrict_universe_context univs vars in
-  let univs = Monomorphic_const_entry univs in
+  let univs = Monomorphic_entry univs in
   mkConst(declare_constant (Id.of_string na) 
             (DefinitionEntry (definition_entry ~opaque:true ~univs c),
 	     IsProof Lemma))