Separate variance and universe fields in inductives.

I think the usage looks cleaner this way.

2 files changed, 11 insertions, 3 deletions

diff --git a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
index 047f4cd080..f5043db099 100644
--- a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
+++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
@@ -9,13 +9,13 @@ let evil t f =
   let u = Level.var 0 in
   let tu = mkType (Universe.make u) in
   let te = Declare.definition_entry
-      ~univs:(Monomorphic_const_entry (ContextSet.singleton u)) tu
+      ~univs:(Monomorphic_entry (ContextSet.singleton u)) tu
   in
   let tc = Declare.declare_constant t (DefinitionEntry te, k) in
   let tc = mkConst tc in
 
   let fe = Declare.definition_entry
-      ~univs:(Polymorphic_const_entry ([|Anonymous|], UContext.make (Instance.of_array [|u|],Constraint.empty)))
+      ~univs:(Polymorphic_entry ([|Anonymous|], UContext.make (Instance.of_array [|u|],Constraint.empty)))
       ~types:(Term.mkArrow tc tu)
       (mkLambda (Name.Name (Id.of_string "x"), tc, mkRel 1))
   in
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index a960fe3441..222a808768 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -1,5 +1,7 @@
 Inductive Empty@{u} : Type@{u} :=  
+(* u |=  *)
 Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A }
+(* u |=  *)
 
 PWrap has primitive projections with eta conversion.
 For PWrap: Argument scope is [type_scope]
@@ -11,6 +13,7 @@ fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p
 
 Argument scopes are [type_scope _]
 Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A }
+(* u |=  *)
 
 For RWrap: Argument scope is [type_scope]
 For rwrap: Argument scopes are [type_scope _]
@@ -79,7 +82,9 @@ Type@{UnivBinders.17} -> Type@{v} -> Type@{u}
      : Type@{max(u+1,UnivBinders.17+1,v+1)}
 (* u UnivBinders.17 v |=  *)
 Inductive Empty@{E} : Type@{E} :=  
+(* E |=  *)
 Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }
+(* E |=  *)
 
 PWrap has primitive projections with eta conversion.
 For PWrap: Argument scope is [type_scope]
@@ -109,7 +114,9 @@ bind_univs.poly@{u} = Type@{u}
 insec@{v} = Type@{u} -> Type@{v}
      : Type@{max(u+1,v+1)}
 (* v |=  *)
-Inductive insecind@{k} : Type@{k+1} :=  inseccstr : Type@{k} -> insecind@{k}
+Inductive insecind@{k} : Type@{k+1} :=
+    inseccstr : Type@{k} -> insecind@{k}
+(* k |=  *)
 
 For inseccstr: Argument scope is [type_scope]
 insec@{u v} = Type@{u} -> Type@{v}
@@ -117,6 +124,7 @@ insec@{u v} = Type@{u} -> Type@{v}
 (* u v |=  *)
 Inductive insecind@{u k} : Type@{k+1} :=
     inseccstr : Type@{k} -> insecind@{u k}
+(* u k |=  *)
 
 For inseccstr: Argument scope is [type_scope]
 insec2@{u} = Prop