From e9b745af47ba3386724b874e3fd74b6dad33b015 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Thu, 6 Apr 2017 22:48:32 +0200
Subject: Allow flexible anonymous universes in instances and sorts.

The addition to the test suite showcases the usage.
---
 test-suite/success/polymorphism.v | 32 +++++++++++++++++++++++++++++++-
 1 file changed, 31 insertions(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 878875bd92..0a58fe89a1 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -321,4 +321,34 @@ Definition unwrap' := fun (X : Type) (b : box X) => let (unw) := b in unw.
 Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _
 Type)) eq_refl.
 
-End Hurkens'.
\ No newline at end of file
+End Hurkens'.
+
+Module Anonymous.
+  Set Universe Polymorphism.
+
+  Definition defaultid := (fun x => x) : Type -> Type.
+  Definition collapseid := defaultid@{_ _}.
+  Check collapseid@{_}.
+
+  Definition anonid := (fun x => x) : Type -> Type@{_}.
+  Check anonid@{_}.
+
+  Definition defaultalg := Type : Type.
+  Definition usedefaultalg := defaultalg@{_ _}.
+  Check usedefaultalg@{_ _}.
+
+  Definition anonalg := (fun x => x) (Type : Type@{_}).
+  Check anonalg@{_}.
+
+  Definition unrelated@{i j} := nat.
+  Definition useunrelated := unrelated@{_ _}.
+  Check useunrelated@{_ _}.
+
+  Definition inthemiddle@{i j k} :=
+    let _ := defaultid@{i j} in
+    defaultalg@{k j}.
+  (* i <= j < k *)
+  Definition collapsethemiddle := inthemiddle@{i _ j}.
+  Check collapsethemiddle@{_ _}.
+
+End Anonymous.
-- 
cgit v1.2.3


From 4361c1ed9ac5646055f9f0eecc4a003d720c1994 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Wed, 12 Apr 2017 13:29:16 +0200
Subject: Type@{_} should not produce a flexible algebraic universe.

Otherwise [(fun x => x) (Type : Type@{_})] becomes
[(fun x : Type@{i+1} => x) (Type@{i} : Type@{i+1})]
breaking the invariant that terms do not contain algebraic universes
(at the lambda abstraction).
---
 test-suite/success/polymorphism.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 0a58fe89a1..66ff55edcb 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -333,12 +333,12 @@ Module Anonymous.
   Definition anonid := (fun x => x) : Type -> Type@{_}.
   Check anonid@{_}.
 
-  Definition defaultalg := Type : Type.
-  Definition usedefaultalg := defaultalg@{_ _}.
+  Definition defaultalg := (fun x : Type => x) (Type : Type).
+  Definition usedefaultalg := defaultalg@{_ _ _}.
   Check usedefaultalg@{_ _}.
 
-  Definition anonalg := (fun x => x) (Type : Type@{_}).
-  Check anonalg@{_}.
+  Definition anonalg := (fun x : Type@{_} => x) (Type : Type).
+  Check anonalg@{_ _}.
 
   Definition unrelated@{i j} := nat.
   Definition useunrelated := unrelated@{_ _}.
@@ -346,7 +346,7 @@ Module Anonymous.
 
   Definition inthemiddle@{i j k} :=
     let _ := defaultid@{i j} in
-    defaultalg@{k j}.
+    anonalg@{k j}.
   (* i <= j < k *)
   Definition collapsethemiddle := inthemiddle@{i _ j}.
   Check collapsethemiddle@{_ _}.
-- 
cgit v1.2.3