aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/output')
-rw-r--r--test-suite/output/Cases.out4
-rw-r--r--test-suite/output/Existentials.out3
-rw-r--r--test-suite/output/InitSyntax.out3
-rw-r--r--test-suite/output/Intuition.out2
-rw-r--r--test-suite/output/Naming.out40
-rw-r--r--test-suite/output/Notations.out14
-rw-r--r--test-suite/output/Notations2.out4
-rw-r--r--test-suite/output/Notations2.v8
-rw-r--r--test-suite/output/PrintInfos.out4
-rw-r--r--test-suite/output/Quote.out18
-rw-r--r--test-suite/output/inference.out8
-rw-r--r--test-suite/output/ltac.out22
-rw-r--r--test-suite/output/ltac.v28
-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, 53 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index f44465456f..2b828d382a 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -6,6 +6,8 @@ fix F (t : t) : P t :=
end
: forall P : t -> Type,
(let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
+
+Argument scopes are [function_scope function_scope _]
= fun d : TT => match d with
| @CTT _ _ b => b
end
@@ -24,7 +26,7 @@ match Nat.eq_dec x y with
end
: forall (x y : nat) (P : nat -> Type), P x -> P y -> P y
-Argument scopes are [nat_scope nat_scope _ _ _]
+Argument scopes are [nat_scope nat_scope function_scope _ _]
foo =
fix foo (A : Type) (l : list A) {struct l} : option A :=
match l with
diff --git a/test-suite/output/Existentials.out b/test-suite/output/Existentials.out
index 52e1e0ed01..9680d2bbff 100644
--- a/test-suite/output/Existentials.out
+++ b/test-suite/output/Existentials.out
@@ -1,5 +1,4 @@
-Existential 1 =
-?Goal1 : [p : nat q := S p : nat n : nat m : nat |- ?y = m]
+Existential 1 = ?Goal : [p : nat q := S p : nat n : nat m : nat |- ?y = m]
Existential 2 =
?y : [p : nat q := S p : nat n : nat m : nat |- nat] (p, q cannot be used)
Existential 3 = ?Goal0 : [q : nat n : nat m : nat |- n = ?y]
diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out
index bbfd3405af..c17c63e724 100644
--- a/test-suite/output/InitSyntax.out
+++ b/test-suite/output/InitSyntax.out
@@ -4,7 +4,8 @@ Inductive sig2 (A : Type) (P Q : A -> Prop) : Type :=
For sig2: Argument A is implicit
For exist2: Argument A is implicit
For sig2: Argument scopes are [type_scope type_scope type_scope]
-For exist2: Argument scopes are [type_scope _ _ _ _ _]
+For exist2: Argument scopes are [type_scope function_scope function_scope _ _
+ _]
exists x : nat, x = x
: Prop
fun b : bool => if b then b else b
diff --git a/test-suite/output/Intuition.out b/test-suite/output/Intuition.out
index e99d9fdebc..f2bf25ca65 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 f0d2562e0f..c142d28ebe 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/Notations.out b/test-suite/output/Notations.out
index b1558dab1c..26eaca8272 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -111,14 +111,14 @@ fun x : option Z => match x with
| NONE2 => 0
end
: option Z -> Z
-fun x : list ?T1 => match x with
- | NIL => NONE2
- | (_ :') t => SOME2 t
- end
- : list ?T1 -> option (list ?T1)
+fun x : list ?T => match x with
+ | NIL => NONE2
+ | (_ :') t => SOME2 t
+ end
+ : list ?T -> option (list ?T)
where
-?T1 : [x : list ?T1 x1 : list ?T1 x0 := x1 : list ?T1 |- Type] (x, x1,
- x0 cannot be used)
+?T : [x : list ?T x1 : list ?T x0 := x1 : list ?T |- Type] (x, x1,
+ x0 cannot be used)
s
: s
10
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 58ec1de563..6ff1d38372 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -50,3 +50,7 @@ end
: nat -> nat
# _ : nat => 2
: nat -> nat
+# x : nat => # H : x <= 0 => exist (le x) 0 H
+ : ∀ x : nat, x <= 0 -> {x0 : nat | x <= x0}
+exist (Q x) y conj
+ : {x0 : A | Q x x0}
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index e53c94ef0a..4e0d135d7d 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -68,6 +68,7 @@ Check let' f x y (a:=0) z (b:bool) := x+y+z+1 in f 0 1 2.
(* In practice, only the printing rule is used here *)
(* Note: does not work for pattern *)
+Module A.
Notation "f ( x )" := (f x) (at level 10, format "f ( x )").
Check fun f x => f x + S x.
@@ -77,6 +78,7 @@ Notation plus2 n := (S (S n)).
(* plus2 was not correctly printed in the two following tests in 8.3pl1 *)
Print plus2.
Check fun n => match n with list1 => 0 | _ => 2 end.
+End A.
(* This one is not fully satisfactory because binders in the same type
are re-factorized and parentheses are needed even for atomic binder
@@ -98,3 +100,9 @@ Notation "# x : T => t" := (fun x : T => t)
Check # x : nat => x.
Check # _ : nat => 2.
+
+(* Check bug 4677 *)
+Check fun x (H:le x 0) => exist (le x) 0 H.
+
+Parameters (A : Set) (x y : A) (Q : A -> A -> Prop) (conj : Q x y).
+Check (exist (Q x) y conj).
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index ba076f050a..98420409e8 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -2,7 +2,7 @@ existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}
existT is template universe polymorphic
Argument A is implicit
-Argument scopes are [type_scope _ _ _]
+Argument scopes are [type_scope function_scope _ _]
Expands to: Constructor Coq.Init.Specif.existT
Inductive sigT (A : Type) (P : A -> Type) : Type :=
existT : forall x : A, P x -> {x : A & P x}
@@ -10,7 +10,7 @@ Inductive sigT (A : Type) (P : A -> Type) : Type :=
For sigT: Argument A is implicit
For existT: Argument A is implicit
For sigT: Argument scopes are [type_scope type_scope]
-For existT: Argument scopes are [type_scope _ _ _]
+For existT: Argument scopes are [type_scope function_scope _ _]
existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}
Argument A is implicit
diff --git a/test-suite/output/Quote.out b/test-suite/output/Quote.out
index ca7fc3624b..998eb37cc8 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/inference.out b/test-suite/output/inference.out
index c5a393408e..576fbd7c0b 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -9,10 +9,10 @@ fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H
fun n : nat => let x := A n : T n in ?y ?y0 : T n
: forall n : nat, T n
where
-?y : [n : nat x := A n : T n |- ?T0 -> T n]
-?y0 : [n : nat x := A n : T n |- ?T0]
+?y : [n : nat x := A n : T n |- ?T -> T n]
+?y0 : [n : nat x := A n : T n |- ?T]
fun n : nat => ?y ?y0 : T n
: forall n : nat, T n
where
-?y : [n : nat |- ?T0 -> T n]
-?y0 : [n : nat |- ?T0]
+?y : [n : nat |- ?T -> T n]
+?y0 : [n : nat |- ?T]
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index d003c70df9..21a8cf9ede 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -1,2 +1,24 @@
The command has indeed failed with message:
Error: Ltac variable y depends on pattern variable name z which is not bound in current context.
+Ltac f x y z :=
+ symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize
+ dependent z
+The command has indeed failed with message:
+In nested Ltac calls to "g1" and "refine", last call failed.
+The term "I" has type "True" while it is expected to have type "False".
+The command has indeed failed with message:
+In nested Ltac calls to "f1" and "refine", last call failed.
+The term "I" has type "True" while it is expected to have type "False".
+The command has indeed failed with message:
+In nested Ltac calls to "g2", "g1" and "refine", last call failed.
+The term "I" has type "True" while it is expected to have type "False".
+The command has indeed failed with message:
+In nested Ltac calls to "f2", "f1" and "refine", last call failed.
+The term "I" has type "True" while it is expected to have type "False".
+The command has indeed failed with message:
+Ltac call to "h" failed.
+Error: Ltac variable x is bound to I which cannot be coerced to
+a declared or quantified hypothesis.
+The command has indeed failed with message:
+In nested Ltac calls to "h" and "injection", last call failed.
+Error: No primitive equality found.
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 7e2610c7d7..dfa60eeda0 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -15,3 +15,31 @@ lazymatch goal with
| H1 : HT |- _ => idtac
end.
Abort.
+
+Ltac f x y z :=
+ symmetry in x, y;
+ auto with z;
+ auto;
+ intros;
+ clearbody x;
+ generalize dependent z.
+
+Print Ltac f.
+
+(* Error messages *)
+
+Ltac g1 x := refine x.
+Tactic Notation "g2" constr(x) := g1 x.
+Tactic Notation "f1" constr(x) := refine x.
+Ltac f2 x := f1 x.
+Goal False.
+Fail g1 I.
+Fail f1 I.
+Fail g2 I.
+Fail f2 I.
+
+Ltac h x := injection x.
+Goal True -> False.
+Fail h I.
+intro H.
+Fail h H.
diff --git a/test-suite/output/set.out b/test-suite/output/set.out
index 4dfd2bc220..4b72d73eb3 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 73888da9a0..526e468f5b 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 0000000000..209b2bc26f
--- /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 0000000000..e48aa6bb28
--- /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.25.1) at 2026-05-02 15:34:18 +0000