From 88ab72280269ce85a2737d91695c75f97b54ee1c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 17 Jun 2014 17:07:38 +0200
Subject: Explicit universes allow to write liftings explicitely. Implicit
 lifting would change the theory non-trivially.

---
 test-suite/bugs/closed/HoTT_coq_093.v | 27 +++++++++++++++++++++++++
 test-suite/bugs/opened/HoTT_coq_093.v | 37 -----------------------------------
 2 files changed, 27 insertions(+), 37 deletions(-)
 create mode 100644 test-suite/bugs/closed/HoTT_coq_093.v
 delete mode 100644 test-suite/bugs/opened/HoTT_coq_093.v

diff --git a/test-suite/bugs/closed/HoTT_coq_093.v b/test-suite/bugs/closed/HoTT_coq_093.v
new file mode 100644
index 0000000000..38943ab353
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_093.v
@@ -0,0 +1,27 @@
+(** It would be nice if we had more lax constraint checking of inductive types, and had variance annotations on their universes *)
+Set Printing All.
+Set Printing Implicit.
+Set Printing Universes.
+Set Universe Polymorphism.
+
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a.
+Arguments idpath {A a} , [A] a.
+
+Notation "x = y" := (@paths _ x y) : type_scope.
+
+Section lift.
+  Let lift_type : Type.
+  Proof.
+    let U0 := constr:(Type) in
+    let U1 := constr:(Type) in
+    let unif := constr:(U0 : U1) in
+    exact (U0 -> U1).
+  Defined.
+
+  Definition Lift (A : Type@{i}) : Type@{j} := A.
+End lift.
+
+Goal forall (A : Type@{i}) (x y : A), @paths@{i} A x y -> @paths@{j} A x y.
+intros A x y p.
+compute in *. destruct p. exact idpath.
+Defined.
diff --git a/test-suite/bugs/opened/HoTT_coq_093.v b/test-suite/bugs/opened/HoTT_coq_093.v
deleted file mode 100644
index 029a0caf76..0000000000
--- a/test-suite/bugs/opened/HoTT_coq_093.v
+++ /dev/null
@@ -1,37 +0,0 @@
-(** It would be nice if we had more lax constraint checking of inductive types, and had variance annotations on their universes *)
-Set Printing All.
-Set Printing Implicit.
-Set Printing Universes.
-Set Universe Polymorphism.
-
-Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a.
-Arguments idpath {A a} , [A] a.
-
-Notation "x = y" := (@paths _ x y) : type_scope.
-
-Section lift.
-  Let lift_type : Type.
-  Proof.
-    let U0 := constr:(Type) in
-    let U1 := constr:(Type) in
-    let unif := constr:(U0 : U1) in
-    exact (U0 -> U1).
-  Defined.
-
-  Definition Lift : lift_type := fun A => A.
-End lift.
-
-Goal forall (A : Type) (x y : A), @paths A x y -> @paths (Lift A) x y.
-intros A x y p.
-compute in *.
-Fail exact p. (* Toplevel input, characters 21-22:
-Error:
-In environment
-A : Type (* Top.15 *)
-x : A
-y : A
-p : @paths (* Top.15 *) A x y
-The term "p" has type "@paths (* Top.15 *) A x y"
-while it is expected to have type "@paths (* Top.18 *) A x y"
-(Universe inconsistency: Cannot enforce Top.18 = Top.15 because Top.15
-< Top.18)). *)
-- 
cgit v1.2.3