aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed')
-rw-r--r--test-suite/bugs/closed/3125.v27
-rw-r--r--test-suite/bugs/closed/3559.v1
-rw-r--r--test-suite/bugs/closed/3690.v75
-rw-r--r--test-suite/bugs/closed/4390.v6
-rw-r--r--test-suite/bugs/closed/5347.v10
-rw-r--r--test-suite/bugs/closed/5717.v5
-rw-r--r--test-suite/bugs/closed/HoTT_coq_064.v1
7 files changed, 82 insertions, 43 deletions
diff --git a/test-suite/bugs/closed/3125.v b/test-suite/bugs/closed/3125.v
new file mode 100644
index 000000000..797146174
--- /dev/null
+++ b/test-suite/bugs/closed/3125.v
@@ -0,0 +1,27 @@
+(* Not considering singleton template-polymorphic inductive types as
+ propositions for injection/inversion *)
+
+(* This is also #4560 and #6273 *)
+
+Inductive foo := foo_1.
+
+Goal forall (a b : foo), Some a = Some b -> a = b.
+Proof.
+ intros a b H.
+ inversion H.
+ reflexivity.
+Qed.
+
+(* Check that Prop is not concerned *)
+
+Inductive bar : Prop := bar_1.
+
+Goal
+ forall (a b : bar),
+ Some a = Some b ->
+ a = b.
+Proof.
+ intros a b H.
+ inversion H.
+ Fail reflexivity.
+Abort.
diff --git a/test-suite/bugs/closed/3559.v b/test-suite/bugs/closed/3559.v
index da12b6868..5210b2703 100644
--- a/test-suite/bugs/closed/3559.v
+++ b/test-suite/bugs/closed/3559.v
@@ -65,6 +65,7 @@ Axiom path_iff_hprop_uncurried : forall `{IsHProp A, IsHProp B}, (A <-> B) -> A
= B.
Inductive V : Type@{U'} := | set {A : Type@{U}} (f : A -> V) : V.
Axiom is0trunc_V : IsTrunc (trunc_S (trunc_S minus_two)) V.
+Existing Instance is0trunc_V.
Axiom bisimulation : V@{U' U} -> V@{U' U} -> hProp@{U'}.
Axiom bisimulation_refl : forall (v : V), bisimulation v v.
Axiom bisimulation_eq : forall (u v : V), bisimulation u v -> u = v.
diff --git a/test-suite/bugs/closed/3690.v b/test-suite/bugs/closed/3690.v
index fd9640b89..fa30132ab 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/4390.v b/test-suite/bugs/closed/4390.v
index a96a13700..c069b2d9d 100644
--- a/test-suite/bugs/closed/4390.v
+++ b/test-suite/bugs/closed/4390.v
@@ -8,16 +8,16 @@ Universe i.
End foo.
End M.
-Check Type@{i}.
+Check Type@{M.i}.
(* Succeeds *)
Fail Check Type@{j}.
(* Error: Undeclared universe: j *)
-Definition foo@{j} : Type@{i} := Type@{j}.
+Definition foo@{j} : Type@{M.i} := Type@{j}.
(* ok *)
End A.
-
+Import A. Import M.
Set Universe Polymorphism.
Fail Universes j.
Monomorphic Universe j.
diff --git a/test-suite/bugs/closed/5347.v b/test-suite/bugs/closed/5347.v
new file mode 100644
index 000000000..9267b3eb6
--- /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 *)
diff --git a/test-suite/bugs/closed/5717.v b/test-suite/bugs/closed/5717.v
new file mode 100644
index 000000000..1bfd917d2
--- /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.
diff --git a/test-suite/bugs/closed/HoTT_coq_064.v b/test-suite/bugs/closed/HoTT_coq_064.v
index b4c745375..d02a5f120 100644
--- a/test-suite/bugs/closed/HoTT_coq_064.v
+++ b/test-suite/bugs/closed/HoTT_coq_064.v
@@ -178,6 +178,7 @@ Definition IsColimit `{Funext} C D (F : Functor D C)
Generalizable All Variables.
Axiom fs : Funext.
+Existing Instance fs.
Section bar.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 01:22:52 +0000