From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- test-suite/bugs/closed/HoTT_coq_093.v | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 test-suite/bugs/closed/HoTT_coq_093.v (limited to 'test-suite/bugs/closed/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 00000000..38943ab3 --- /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. -- cgit v1.2.3