Explicit universes allow to write liftings explicitely. Implicit lifting would change the

theory non-trivially.

1 files changed, 0 insertions, 37 deletions

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 029a0caf7..000000000
--- 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)). *)