From c93d5094bff73498ec8fc02837e16cc5ce9103b6 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 7 Sep 2017 16:56:34 +0200
Subject: Make restrict_universe_context stronger.

This fixes BZ#5717.

Also add a test and fix a changed test.
---
 test-suite/bugs/closed/3690.v | 75 ++++++++++++++++++++-----------------------
 test-suite/bugs/closed/5717.v |  5 +++
 2 files changed, 40 insertions(+), 40 deletions(-)
 create mode 100644 test-suite/bugs/closed/5717.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/3690.v b/test-suite/bugs/closed/3690.v
index fd9640b890..fa30132ab5 100644
--- a/test-suite/bugs/closed/3690.v
+++ b/test-suite/bugs/closed/3690.v
@@ -3,49 +3,44 @@ Set Printing Universes.
 Set Universe Polymorphism.
 Definition foo (a := Type) (b := Type) (c := Type) := Type.
 Print foo.
-(* foo =
-let a := Type@{Top.1} in
-let b := Type@{Top.2} in let c := Type@{Top.3} in Type@{Top.4}
-     : Type@{Top.4+1}
-(* Top.1
-   Top.2
-   Top.3
-   Top.4 |=  *) *)
-Check @foo. (* foo@{Top.5 Top.6 Top.7
-Top.8}
-     : Type@{Top.8+1}
-(* Top.5
-   Top.6
-   Top.7
-   Top.8 |=  *) *)
+(* foo@{Top.2 Top.3 Top.5 Top.6 Top.8 Top.9 Top.10} =
+let a := Type@{Top.2} in let b := Type@{Top.5} in let c := Type@{Top.8} in Type@{Top.10}
+     : Type@{Top.10+1}
+(* Top.2 Top.3 Top.5 Top.6 Top.8 Top.9 Top.10 |= Top.2 < Top.3
+                                                 Top.5 < Top.6
+                                                 Top.8 < Top.9
+                                                  *)
+ *)
+Check @foo. (* foo@{Top.11 Top.12 Top.13 Top.14 Top.15 Top.16
+Top.17}
+     : Type@{Top.17+1}
+(* Top.11 Top.12 Top.13 Top.14 Top.15 Top.16 Top.17 |= Top.11 < Top.12
+                                                       Top.13 < Top.14
+                                                       Top.15 < Top.16
+                                                        *)
+ *)
 Definition bar := ltac:(let t := eval compute in foo in exact t).
-Check @bar. (* bar@{Top.13 Top.14 Top.15
-Top.16}
-     : Type@{Top.16+1}
-(* Top.13
-   Top.14
-   Top.15
-   Top.16 |=  *) *)
-(* The following should fail, since [bar] should only need one universe. *)
-Check @bar@{i j}.
+Check @bar. (* bar@{Top.27}
+     : Type@{Top.27+1}
+(* Top.27 |=  *) *)
+
+Check @bar@{i}.
 Definition baz (a := Type) (b := Type : a) (c := Type : b) := a -> c.
 Definition qux := Eval compute in baz.
-Check @qux. (* qux@{Top.24 Top.25
-Top.26}
-     : Type@{max(Top.24+1, Top.26+1)}
-(* Top.24
-   Top.25
-   Top.26 |= Top.25 < Top.24
-              Top.26 < Top.25
-               *) *)
-Print qux. (* qux =
-Type@{Top.21} -> Type@{Top.23}
-     : Type@{max(Top.21+1, Top.23+1)}
-(* Top.21
-   Top.22
-   Top.23 |= Top.22 < Top.21
-              Top.23 < Top.22
-               *) *)
+Check @qux. (* qux@{Top.38 Top.39 Top.40
+Top.41}
+     : Type@{max(Top.38+1, Top.41+1)}
+(* Top.38 Top.39 Top.40 Top.41 |= Top.38 < Top.39
+                                  Top.40 < Top.38
+                                  Top.41 < Top.40
+                                   *) *)
+Print qux. (* qux@{Top.34 Top.35 Top.36 Top.37} =
+Type@{Top.34} -> Type@{Top.37}
+     : Type@{max(Top.34+1, Top.37+1)}
+(* Top.34 Top.35 Top.36 Top.37 |= Top.34 < Top.35
+                                  Top.36 < Top.34
+                                  Top.37 < Top.36
+                                   *) *)
 Fail Check @qux@{Set Set}.
 Check @qux@{Type Type Type Type}.
 (* [qux] should only need two universes *)
diff --git a/test-suite/bugs/closed/5717.v b/test-suite/bugs/closed/5717.v
new file mode 100644
index 0000000000..1bfd917d25
--- /dev/null
+++ b/test-suite/bugs/closed/5717.v
@@ -0,0 +1,5 @@
+Definition foo@{i} (A : Type@{i}) (l : list A) :=
+  match l with
+  | nil => nil
+  | cons _ t => t
+  end.
-- 
cgit v1.2.3


From 4940f99922b0784d726b7c50abe63395713f012f Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 17 Nov 2017 23:48:21 +0100
Subject: Fix #5347: unify declaration of axioms with and without bound univs.

Note that this makes the following syntax valid:

     Axiom foo@{i} bar : Type@{i}.

(ie putting a universe declaration on the first axiom in the list, the
declaration then holds for the whole list).
---
 test-suite/bugs/closed/5347.v | 10 ++++++++++
 1 file changed, 10 insertions(+)
 create mode 100644 test-suite/bugs/closed/5347.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/5347.v b/test-suite/bugs/closed/5347.v
new file mode 100644
index 0000000000..9267b3eb69
--- /dev/null
+++ b/test-suite/bugs/closed/5347.v
@@ -0,0 +1,10 @@
+Set Universe Polymorphism.
+
+Axiom X : Type.
+(* Used to declare [x0@{u1 u2} : X@{u1}] and [x1@{} : X@{u2}] leaving
+   the type of x1 with undeclared universes. After PR #891 this should
+   error at declaration time. *)
+Axiom x₀ x₁ : X.
+Axiom Xᵢ : X -> Type.
+
+Check Xᵢ x₁. (* conversion test raised anomaly universe undefined *)
-- 
cgit v1.2.3