diff options
Diffstat (limited to 'test-suite/bugs')
-rw-r--r-- | test-suite/bugs/closed/HoTT_coq_074.v | 10 | ||||
-rw-r--r-- | test-suite/bugs/closed/HoTT_coq_114.v | 1 | ||||
-rw-r--r-- | test-suite/bugs/opened/HoTT_coq_074.v | 12 | ||||
-rw-r--r-- | test-suite/bugs/opened/HoTT_coq_114.v | 2 |
4 files changed, 11 insertions, 14 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_074.v b/test-suite/bugs/closed/HoTT_coq_074.v new file mode 100644 index 000000000..370c7d404 --- /dev/null +++ b/test-suite/bugs/closed/HoTT_coq_074.v @@ -0,0 +1,10 @@ +Monomorphic Definition U1 := Type. +Monomorphic Definition U2 := Type. + +Set Printing Universes. +Definition foo : True. +let t1 := type of U1 in +let t2 := type of U2 in +idtac t1 t2; +pose (t1 : t2). exact I. +Defined. diff --git a/test-suite/bugs/closed/HoTT_coq_114.v b/test-suite/bugs/closed/HoTT_coq_114.v new file mode 100644 index 000000000..341128338 --- /dev/null +++ b/test-suite/bugs/closed/HoTT_coq_114.v @@ -0,0 +1 @@ +Inductive test : $(let U := type of Type in exact U)$ := t. diff --git a/test-suite/bugs/opened/HoTT_coq_074.v b/test-suite/bugs/opened/HoTT_coq_074.v deleted file mode 100644 index 7c88447b2..000000000 --- a/test-suite/bugs/opened/HoTT_coq_074.v +++ /dev/null @@ -1,12 +0,0 @@ -Monomorphic Definition U1 := Type. -Monomorphic Definition U2 := Type. - -Set Printing Universes. -Definition foo : True. -Fail let t1 := type of U1 in -let t2 := type of U2 in -pose (t1 : t2). (* Error: -The term "Type (* Top.1+1 *)" has type "Type (* Top.1+2 *)" -while it is expected to have type "Type (* Top.2+1 *)". *) -exact I. -Defined. diff --git a/test-suite/bugs/opened/HoTT_coq_114.v b/test-suite/bugs/opened/HoTT_coq_114.v deleted file mode 100644 index e293e6dbb..000000000 --- a/test-suite/bugs/opened/HoTT_coq_114.v +++ /dev/null @@ -1,2 +0,0 @@ -Fail Inductive test : $(let U := type of Type in exact U)$ := t. -(* Anomaly: Unable to handle arbitrary u+k <= v constraints. Please report. *) |