Merge PR #8760: Automatically generate names for universes.

3 files changed, 10 insertions, 18 deletions

diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 178116c580..d63b6dbfce 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -79,8 +79,9 @@ mono
 The command has indeed failed with message:
 Universe u already exists.
 Monomorphic bobmorane = 
-let tt := Type@{tt.v} in let ff := Type@{ff.v} in tt -> ff
-     : Type@{max(tt.u,ff.u)}
+let tt := Type@{UnivBinders.32} in
+let ff := Type@{UnivBinders.34} in tt -> ff
+     : Type@{max(UnivBinders.31,UnivBinders.33)}
 
 bobmorane is not universe polymorphic
 The command has indeed failed with message:
@@ -190,12 +191,12 @@ Type@{UnivBinders.57} -> Type@{i}
 axbar is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant UnivBinders.axbar
-axfoo' : Type@{UnivBinders.59} -> Type@{axbar'.i}
+axfoo' : Type@{axbar'.u0} -> Type@{axbar'.i}
 
 axfoo' is not universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant UnivBinders.axfoo'
-axbar' : Type@{UnivBinders.59} -> Type@{axbar'.i}
+axbar' : Type@{axbar'.u0} -> 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 ad901da72f..582a5e969a 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -74,19 +74,10 @@ Module SecLet.
     (* Fail Let foo@{} := Type@{u}. (* doesn't parse: Let foo@{...} doesn't exist *) *)
     Unset Strict Universe Declaration.
     Let tt : Type@{u} := Type@{v}. (* names disappear in the ether *)
-    Let ff : Type@{u}. Proof. exact Type@{v}. Qed. (* if Set Universe Polymorphism: universes are named ff.u and ff.v. Otherwise names disappear into space *)
+    Let ff : Type@{u}. Proof. exact Type@{v}. Qed. (* names disappear into space *)
     Definition bobmorane := tt -> ff.
   End foo.
-  Print bobmorane. (*
-                     bobmorane@{UnivBinders.15 UnivBinders.16 ff.u ff.v} =
-                     let tt := Type@{UnivBinders.16} in let ff := Type@{ff.v} in tt -> ff
-                     : Type@{max(UnivBinders.15,ff.u)}
-                     (* UnivBinders.15 UnivBinders.16 ff.u ff.v |= UnivBinders.16 < UnivBinders.15
-                     ff.v < ff.u
-                    *)
-
-                    bobmorane is universe polymorphic
-                    *)
+  Print bobmorane.
 End SecLet.
 
 (* fun x x => foo is nonsense with local binders *)
diff --git a/test-suite/success/unidecls.v b/test-suite/success/unidecls.v
index 7c298c98b6..1bc565cbb5 100644
--- a/test-suite/success/unidecls.v
+++ b/test-suite/success/unidecls.v
@@ -1,4 +1,4 @@
-(* coq-prog-args: ("-top" "unidecls") *)
+(* -*- coq-prog-args: ("-top" "unidecls"); -*- *)
 Set Printing Universes.
 
 Module decls.
@@ -46,12 +46,12 @@ Universe secfoo.
 Section Foo'.
   Fail Universe secfoo.
   Universe secfoo2.
-  Check Type@{Foo'.secfoo2}.
+  Fail Check Type@{Foo'.secfoo2}.
+  Check Type@{secfoo2}.
   Constraint secfoo2 < a.
 End Foo'.
 
 Check Type@{secfoo2}.
-Fail Check Type@{Foo'.secfoo2}.
 Fail Check eq_refl : Type@{secfoo2} = Type@{a}.
 
 (** Below, u and v are global, fixed universes *)