Merge PR #8601: Move bound universe names to abstract contexts

3 files changed, 20 insertions, 9 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 6d8ce7c5d7..047f4cd080 100644
--- a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
+++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
@@ -15,7 +15,7 @@ let evil t f =
   let tc = mkConst tc in
 
   let fe = Declare.definition_entry
-      ~univs:(Polymorphic_const_entry (UContext.make (Instance.of_array [|u|],Constraint.empty)))
+      ~univs:(Polymorphic_const_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 49c292c501..178116c580 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -150,6 +150,11 @@ Polymorphic NonCumulative Inductive insecind@{u k} : Type@{k+1} :=
     inseccstr : Type@{k} -> insecind@{u k}
 
 For inseccstr: Argument scope is [type_scope]
+Polymorphic insec2@{u} = Prop
+     : Type@{Set+1}
+(* u |=  *)
+
+insec2 is universe polymorphic
 Polymorphic inmod@{u} = Type@{u}
      : Type@{u+1}
 (* u |=  *)
@@ -171,26 +176,26 @@ inmod@{u} -> Type@{v}
 (* u v |=  *)
 
 Applied.infunct is universe polymorphic
-axfoo@{i UnivBinders.55 UnivBinders.56} :
-Type@{UnivBinders.55} -> Type@{i}
-(* i UnivBinders.55 UnivBinders.56 |=  *)
+axfoo@{i UnivBinders.56 UnivBinders.57} :
+Type@{UnivBinders.56} -> Type@{i}
+(* i UnivBinders.56 UnivBinders.57 |=  *)
 
 axfoo is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant UnivBinders.axfoo
-axbar@{i UnivBinders.55 UnivBinders.56} :
-Type@{UnivBinders.56} -> Type@{i}
-(* i UnivBinders.55 UnivBinders.56 |=  *)
+axbar@{i UnivBinders.56 UnivBinders.57} :
+Type@{UnivBinders.57} -> Type@{i}
+(* i UnivBinders.56 UnivBinders.57 |=  *)
 
 axbar is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant UnivBinders.axbar
-axfoo' : Type@{UnivBinders.58} -> Type@{axbar'.i}
+axfoo' : Type@{UnivBinders.59} -> Type@{axbar'.i}
 
 axfoo' is not universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant UnivBinders.axfoo'
-axbar' : Type@{UnivBinders.58} -> Type@{axbar'.i}
+axbar' : Type@{UnivBinders.59} -> Type@{axbar'.i}
 
 axbar' is not universe polymorphic
 Argument scope is [type_scope]
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index 56474a0723..19d241d35d 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -130,6 +130,12 @@ End SomeSec.
 Print insec.
 Print insecind.
 
+Section SomeSec2.
+  Universe u.
+  Definition insec2@{} := Prop.
+End SomeSec2.
+Print insec2.
+
 Module SomeMod.
   Definition inmod@{u} := Type@{u}.
   Print inmod.