aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bugs/closed/3825.v16
-rw-r--r--test-suite/bugs/closed/3922.v2
-rw-r--r--test-suite/bugs/closed/4292.v7
-rw-r--r--test-suite/bugs/closed/4538.v1
-rw-r--r--test-suite/bugs/closed/4544.v2
-rw-r--r--test-suite/bugs/closed/4576.v3
-rw-r--r--test-suite/bugs/closed/4616.v4
-rw-r--r--test-suite/bugs/closed/4663.v3
-rw-r--r--test-suite/bugs/closed/4670.v7
-rw-r--r--test-suite/bugs/closed/4695.v38
-rw-r--r--test-suite/output/Intuition.out2
-rw-r--r--test-suite/output/Naming.out40
-rw-r--r--test-suite/output/Quote.out18
-rw-r--r--test-suite/output/set.out6
-rw-r--r--test-suite/output/simpl.out6
-rw-r--r--test-suite/output/subst.out97
-rw-r--r--test-suite/output/subst.v48
17 files changed, 262 insertions, 38 deletions
diff --git a/test-suite/bugs/closed/3825.v b/test-suite/bugs/closed/3825.v
new file mode 100644
index 000000000..e594b74b6
--- /dev/null
+++ b/test-suite/bugs/closed/3825.v
@@ -0,0 +1,16 @@
+Set Universe Polymorphism.
+Set Printing Universes.
+
+Axiom foo@{i j} : Type@{i} -> Type@{j}.
+
+Notation bar := foo.
+
+Monomorphic Universes i j.
+
+Check bar@{i j}.
+Fail Check bar@{i}.
+
+Notation qux := (nat -> nat).
+
+Fail Check qux@{i}.
+
diff --git a/test-suite/bugs/closed/3922.v b/test-suite/bugs/closed/3922.v
index 5013bc6ac..d88e8c332 100644
--- a/test-suite/bugs/closed/3922.v
+++ b/test-suite/bugs/closed/3922.v
@@ -73,7 +73,7 @@ Definition Trunc_ind {n A}
(P : Trunc n A -> Type) {Pt : forall aa, IsTrunc n (P aa)}
: (forall a, P (tr a)) -> (forall aa, P aa)
:= (fun f aa => match aa with tr a => fun _ => f a end Pt).
-Definition merely (A : Type@{i}) : hProp@{i} := BuildhProp (Trunc -1 A).
+Definition merely (A : Type@{i}) : hProp := BuildhProp (Trunc -1 A).
Definition cconst_factors_contr `{Funext} {X Y : Type} (f : X -> Y)
(P : Type) `{Pc : X -> Contr P}
(g : X -> P) (h : P -> Y) (p : h o g == f)
diff --git a/test-suite/bugs/closed/4292.v b/test-suite/bugs/closed/4292.v
new file mode 100644
index 000000000..403e155ea
--- /dev/null
+++ b/test-suite/bugs/closed/4292.v
@@ -0,0 +1,7 @@
+Module Type S. End S.
+
+Declare Module M : S.
+
+Module Type F (T: S). End F.
+
+Fail Module Type N := F with Module T := M.
diff --git a/test-suite/bugs/closed/4538.v b/test-suite/bugs/closed/4538.v
new file mode 100644
index 000000000..f925aae9e
--- /dev/null
+++ b/test-suite/bugs/closed/4538.v
@@ -0,0 +1 @@
+Reserved Notation " (u *) ".
diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v
index d14cc86fc..048f31ce3 100644
--- a/test-suite/bugs/closed/4544.v
+++ b/test-suite/bugs/closed/4544.v
@@ -841,7 +841,7 @@ End Truncation_Modalities.
Module Import TrM := Modalities_Theory Truncation_Modalities.
-Definition merely (A : Type@{i}) : hProp@{i} := BuildhProp (Trunc -1 A).
+Definition merely (A : Type@{i}) : hProp := BuildhProp (Trunc -1 A).
Notation IsSurjection := (IsConnMap -1).
diff --git a/test-suite/bugs/closed/4576.v b/test-suite/bugs/closed/4576.v
new file mode 100644
index 000000000..2c643ea77
--- /dev/null
+++ b/test-suite/bugs/closed/4576.v
@@ -0,0 +1,3 @@
+Definition foo := O.
+Arguments foo : simpl nomatch.
+Timeout 1 Eval cbn in id foo.
diff --git a/test-suite/bugs/closed/4616.v b/test-suite/bugs/closed/4616.v
new file mode 100644
index 000000000..c862f8206
--- /dev/null
+++ b/test-suite/bugs/closed/4616.v
@@ -0,0 +1,4 @@
+Set Primitive Projections.
+Record Foo' := Foo { foo : Type }.
+Axiom f : forall t : Foo', foo t.
+Extraction f.
diff --git a/test-suite/bugs/closed/4663.v b/test-suite/bugs/closed/4663.v
new file mode 100644
index 000000000..b76619882
--- /dev/null
+++ b/test-suite/bugs/closed/4663.v
@@ -0,0 +1,3 @@
+Coercion foo (n : nat) : Set.
+Admitted.
+Check (0 : Set).
diff --git a/test-suite/bugs/closed/4670.v b/test-suite/bugs/closed/4670.v
new file mode 100644
index 000000000..611399295
--- /dev/null
+++ b/test-suite/bugs/closed/4670.v
@@ -0,0 +1,7 @@
+Require Import Coq.Vectors.Vector.
+Module Bar.
+ Definition foo A n (l : Vector.t A n) : True.
+ Proof.
+ induction l ; exact I.
+ Defined.
+End Bar.
diff --git a/test-suite/bugs/closed/4695.v b/test-suite/bugs/closed/4695.v
new file mode 100644
index 000000000..a42271811
--- /dev/null
+++ b/test-suite/bugs/closed/4695.v
@@ -0,0 +1,38 @@
+(*
+The Qed at the end of this file was slow in 8.5 and 8.5pl1 because the kernel
+term comparison after evaluation was done on constants according to their user
+names. The conversion still succeeded because delta applied, but was much
+slower than with a canonical names comparison.
+*)
+
+Module Mod0.
+
+ Fixpoint rec_ t d : nat :=
+ match d with
+ | O => O
+ | S d' =>
+ match t with
+ | true => rec_ t d'
+ | false => rec_ t d'
+ end
+ end.
+
+ Definition depth := 1000.
+
+ Definition rec t := rec_ t depth.
+
+End Mod0.
+
+
+Module Mod1.
+ Module M := Mod0.
+End Mod1.
+
+
+Axiom rec_prop : forall t d n, Mod1.M.rec_ t d = n.
+
+Lemma slow_qed : forall t n,
+ Mod0.rec t = n.
+Proof.
+ intros; unfold Mod0.rec; apply rec_prop.
+Timeout 2 Qed.
diff --git a/test-suite/output/Intuition.out b/test-suite/output/Intuition.out
index e99d9fdeb..f2bf25ca6 100644
--- a/test-suite/output/Intuition.out
+++ b/test-suite/output/Intuition.out
@@ -3,4 +3,4 @@
m, n : Z
H : (m >= n)%Z
============================
- (m >= m)%Z
+ (m >= m)%Z
diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out
index f0d2562e0..c142d28eb 100644
--- a/test-suite/output/Naming.out
+++ b/test-suite/output/Naming.out
@@ -2,40 +2,40 @@
x3 : nat
============================
- forall x x1 x4 x0 : nat,
- (forall x2 x5 : nat, x2 + x1 = x4 + x5) -> x + x1 = x4 + x0
+ forall x x1 x4 x0 : nat,
+ (forall x2 x5 : nat, x2 + x1 = x4 + x5) -> x + x1 = x4 + x0
1 subgoal
x3, x, x1, x4, x0 : nat
H : forall x x3 : nat, x + x1 = x4 + x3
============================
- x + x1 = x4 + x0
+ x + x1 = x4 + x0
1 subgoal
x3 : nat
============================
- forall x x1 x4 x0 : nat,
- (forall x2 x5 : nat, x2 + x1 = x4 + x5 -> foo (S x2 + x1)) ->
- x + x1 = x4 + x0 -> foo (S x)
+ forall x x1 x4 x0 : nat,
+ (forall x2 x5 : nat, x2 + x1 = x4 + x5 -> foo (S x2 + x1)) ->
+ x + x1 = x4 + x0 -> foo (S x)
1 subgoal
x3 : nat
============================
- forall x x1 x4 x0 : nat,
- (forall x2 x5 : nat,
- x2 + x1 = x4 + x5 ->
- forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) ->
- x + x1 = x4 + x0 ->
- forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
+ forall x x1 x4 x0 : nat,
+ (forall x2 x5 : nat,
+ x2 + x1 = x4 + x5 ->
+ forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) ->
+ x + x1 = x4 + x0 ->
+ forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
1 subgoal
x3, x, x1, x4, x0 : nat
============================
- (forall x2 x5 : nat,
- x2 + x1 = x4 + x5 ->
- forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) ->
- x + x1 = x4 + x0 ->
- forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
+ (forall x2 x5 : nat,
+ x2 + x1 = x4 + x5 ->
+ forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) ->
+ x + x1 = x4 + x0 ->
+ forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
1 subgoal
x3, x, x1, x4, x0 : nat
@@ -44,7 +44,7 @@
forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + x1)
H0 : x + x1 = x4 + x0
============================
- forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
+ forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
1 subgoal
x3, x, x1, x4, x0 : nat
@@ -54,10 +54,10 @@
H0 : x + x1 = x4 + x0
x5, x6, x7, S : nat
============================
- x5 + S = x6 + x7 + Datatypes.S x
+ x5 + S = x6 + x7 + Datatypes.S x
1 subgoal
x3, a : nat
H : a = 0 -> forall a : nat, a = 0
============================
- a = 0
+ a = 0
diff --git a/test-suite/output/Quote.out b/test-suite/output/Quote.out
index ca7fc3624..998eb37cc 100644
--- a/test-suite/output/Quote.out
+++ b/test-suite/output/Quote.out
@@ -8,17 +8,17 @@
H : interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx) \/
B
============================
- interp_f
- (Node_vm B (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (Empty_vm Prop))
- (f_and (f_atom (Left_idx End_idx))
- (f_and (f_or (f_atom End_idx) (f_atom (Left_idx End_idx)))
- (f_or (f_atom (Left_idx End_idx)) (f_not (f_atom End_idx)))))
+ interp_f
+ (Node_vm B (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (Empty_vm Prop))
+ (f_and (f_atom (Left_idx End_idx))
+ (f_and (f_or (f_atom End_idx) (f_atom (Left_idx End_idx)))
+ (f_or (f_atom (Left_idx End_idx)) (f_not (f_atom End_idx)))))
1 subgoal
H : interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx) \/
B
============================
- interp_f (Node_vm B (Empty_vm Prop) (Empty_vm Prop))
- (f_and (f_const A)
- (f_and (f_or (f_atom End_idx) (f_const A))
- (f_or (f_const A) (f_not (f_atom End_idx)))))
+ interp_f (Node_vm B (Empty_vm Prop) (Empty_vm Prop))
+ (f_and (f_const A)
+ (f_and (f_or (f_atom End_idx) (f_const A))
+ (f_or (f_const A) (f_not (f_atom End_idx)))))
diff --git a/test-suite/output/set.out b/test-suite/output/set.out
index 4dfd2bc22..4b72d73eb 100644
--- a/test-suite/output/set.out
+++ b/test-suite/output/set.out
@@ -3,16 +3,16 @@
y1 := 0 : nat
x := 0 + 0 : nat
============================
- x = x
+ x = x
1 subgoal
y1, y2 := 0 : nat
x := y2 + 0 : nat
============================
- x = x
+ x = x
1 subgoal
y1, y2, y3 := 0 : nat
x := y2 + y3 : nat
============================
- x = x
+ x = x
diff --git a/test-suite/output/simpl.out b/test-suite/output/simpl.out
index 73888da9a..526e468f5 100644
--- a/test-suite/output/simpl.out
+++ b/test-suite/output/simpl.out
@@ -2,14 +2,14 @@
x : nat
============================
- x = S x
+ x = S x
1 subgoal
x : nat
============================
- 0 + x = S x
+ 0 + x = S x
1 subgoal
x : nat
============================
- x = 1 + x
+ x = 1 + x
diff --git a/test-suite/output/subst.out b/test-suite/output/subst.out
new file mode 100644
index 000000000..209b2bc26
--- /dev/null
+++ b/test-suite/output/subst.out
@@ -0,0 +1,97 @@
+1 subgoal
+
+ y, z : nat
+ Hy : y = 0
+ Hz : z = 0
+ H1 : 0 = 1
+ HA : True
+ H2 : 0 = 2
+ H3 : y = 3
+ HB : True
+ H4 : z = 4
+ ============================
+ True
+1 subgoal
+
+ x, z : nat
+ Hx : x = 0
+ Hz : z = 0
+ H1 : x = 1
+ HA : True
+ H2 : x = 2
+ H3 : 0 = 3
+ HB : True
+ H4 : z = 4
+ ============================
+ True
+1 subgoal
+
+ x, y : nat
+ Hx : x = 0
+ Hy : y = 0
+ H1 : x = 1
+ HA : True
+ H2 : x = 2
+ H3 : y = 3
+ HB : True
+ H4 : 0 = 4
+ ============================
+ True
+1 subgoal
+
+ H1 : 0 = 1
+ HA : True
+ H2 : 0 = 2
+ H3 : 0 = 3
+ HB : True
+ H4 : 0 = 4
+ ============================
+ True
+1 subgoal
+
+ y, z : nat
+ Hy : y = 0
+ Hz : z = 0
+ HA : True
+ H3 : y = 3
+ HB : True
+ H4 : z = 4
+ H1 : 0 = 1
+ H2 : 0 = 2
+ ============================
+ True
+1 subgoal
+
+ x, z : nat
+ Hx : x = 0
+ Hz : z = 0
+ H1 : x = 1
+ HA : True
+ H2 : x = 2
+ HB : True
+ H4 : z = 4
+ H3 : 0 = 3
+ ============================
+ True
+1 subgoal
+
+ x, y : nat
+ Hx : x = 0
+ Hy : y = 0
+ H1 : x = 1
+ HA : True
+ H2 : x = 2
+ H3 : y = 3
+ HB : True
+ H4 : 0 = 4
+ ============================
+ True
+1 subgoal
+
+ HA, HB : True
+ H4 : 0 = 4
+ H3 : 0 = 3
+ H1 : 0 = 1
+ H2 : 0 = 2
+ ============================
+ True
diff --git a/test-suite/output/subst.v b/test-suite/output/subst.v
new file mode 100644
index 000000000..e48aa6bb2
--- /dev/null
+++ b/test-suite/output/subst.v
@@ -0,0 +1,48 @@
+(* Ensure order of hypotheses is respected after "subst" *)
+
+Set Regular Subst Tactic.
+Goal forall x y z, x = 0 -> y = 0 -> z = 0 -> x = 1 -> True -> x = 2 -> y = 3 -> True -> z = 4 -> True.
+intros * Hx Hy Hz H1 HA H2 H3 HB H4.
+(* From now on, the order after subst is consistently H1, HA, H2, H3, HB, H4 *)
+subst x.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, H3, HB, H4, H1, H2 *)
+Show.
+Undo.
+subst y.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, HB, H4, H3 *)
+Show.
+Undo.
+subst z.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, H3, HB, H4 *)
+Show.
+Undo.
+subst.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, HB, H4, H3, H1, H2 *)
+(* In 8.5pl0 and 8.5pl1 with regular subst tactic mode, the order was HA, HB, H1, H2, H3, H4 *)
+Show.
+trivial.
+Qed.
+
+Unset Regular Subst Tactic.
+Goal forall x y z, x = 0 -> y = 0 -> z = 0 -> x = 1 -> True -> x = 2 -> y = 3 -> True -> z = 4 -> True.
+intros * Hx Hy Hz H1 HA H2 H3 HB H4.
+subst x.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, H3, HB, H4, H1, H2 *)
+Show.
+Undo.
+subst y.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, HB, H4, H3 *)
+Show.
+Undo.
+subst z.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, H3, HB, H4 *)
+Show.
+Undo.
+subst.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, HB, H4, H3, H1, H2 *)
+(* In 8.5pl0 and 8.5pl1 with regular subst tactic mode, the order was HA, HB, H1, H2, H3, H4 *)
+Show.
+trivial.
+Qed.
+
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 10:12:48 +0000