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

2 files changed, 19 insertions, 8 deletions

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.