diff options
Diffstat (limited to 'test-suite')
58 files changed, 478 insertions, 237 deletions
diff --git a/test-suite/bugs/closed/bug_13413.v b/test-suite/bugs/closed/bug_13413.v new file mode 100644 index 0000000000..b4414a6a1d --- /dev/null +++ b/test-suite/bugs/closed/bug_13413.v @@ -0,0 +1,20 @@ +Goal forall (A B : Prop) (H : A -> B), A -> A -> B. +intros A B H ?%H H0. +exact H1. +Qed. + +Goal forall (A B : Prop) (H : A -> B), A -> A -> B. +intros A B H ?H%H H0. +exact H1. +Qed. + +Goal forall (A B : Prop) (H : A -> B), A -> A -> B. +intros A B H J%H H0. +exact J. +Qed. + +Set Mangle Names. +Goal forall (A B : Prop) (H : A -> B), A -> A -> B. +intros A B H ?%H _0. +assumption. +Qed. diff --git a/test-suite/bugs/closed/bug_13755.v b/test-suite/bugs/closed/bug_13755.v new file mode 100644 index 0000000000..cc25157b9b --- /dev/null +++ b/test-suite/bugs/closed/bug_13755.v @@ -0,0 +1,5 @@ +Module M1. +Lemma t1 : True. +Fail End M1. +Proof. exact I. Qed. +End M1. diff --git a/test-suite/micromega/bug_13794.v b/test-suite/micromega/bug_13794.v new file mode 100644 index 0000000000..5e303a0b7f --- /dev/null +++ b/test-suite/micromega/bug_13794.v @@ -0,0 +1,39 @@ +From Coq Require Import Lia ZArith.ZArith NArith.NArith. +Unset Nia Cache. + +Open Scope N_scope. + + +Lemma over (n0 n1 n2 n3 n4 n5 n6 : N) + (e0 : 1 + 8 * n0 = n1 * n1 + n2) + (e1 : n1 - 1 = 2 * n3 + n4) + (e2 : n3 * (1 + n3) = 2 * n5) + (e3 : n2 + 2 * n4 * n1 - n4 = 8 * n6) + (o0 : n4 = 0 \/ n4 = 1) : + n6 = n0 - n5. +Proof. + Time nia. +Qed. + +Lemma over2 (n0 n1 n2 n3 n4 n5 n6 : N) + (e0 : 1 + 8 * n0 = n1 * n1 + n2) + (e1 : n1 + 1 = 2 * n3 + n4) + (e2 : n3 * (1 + n3) = 2 * n5) + (e3 : n2 + 2 * n4 * n1 + n4 = 8 * n6) + (o0 : n4 = 0) : + n6 = n0 + n5. +Proof. + Fail nia. +Abort. + +Open Scope Z_scope. + +Lemma over3 (n1 n2 n3 n4 n5 : Z) + (e : 0 <= n1 /\ 0 <= n2 /\ 0 <= n3 /\ 0 <= n4 + /\ 0 <= n5) + (e1 : n1 + 1 = 20 * n3 + n4) + (e3 : n2 + 2 * n4 * n1 + n4 = 8 * n5) : + n5 = 0. +Proof. +Time Fail nia. +Abort. diff --git a/test-suite/misc/non-marshalable-state.sh b/test-suite/misc/non-marshalable-state.sh new file mode 100755 index 0000000000..eef7786ebc --- /dev/null +++ b/test-suite/misc/non-marshalable-state.sh @@ -0,0 +1,30 @@ +#!/usr/bin/env bash + +set -e + +export COQBIN=$BIN +export PATH=$COQBIN:$PATH + +cd misc/non-marshalable-state/ + +coq_makefile -f _CoqProject -o Makefile + +make clean + +make src/evil_plugin.cmxs +make src/good_plugin.cmxs + +RC=1 +# must fail +coqc -async-proofs on -I src -Q theories Marshal theories/evil.v 2> log1 1>&2 || RC=0 +# for this reason +grep -q 'Marshalling error' log1 || RC=1 + +# must work +coqc -async-proofs off -I src -Q theories Marshal theories/evil.v + +# must work +coqc -async-proofs on -I src -Q theories Marshal theories/good.v + + +exit $RC diff --git a/test-suite/misc/non-marshalable-state/_CoqProject b/test-suite/misc/non-marshalable-state/_CoqProject new file mode 100644 index 0000000000..09e68d866c --- /dev/null +++ b/test-suite/misc/non-marshalable-state/_CoqProject @@ -0,0 +1,9 @@ +-Q theories Marshal +-I src + +src/evil.mlg +src/good.mlg +src/evil_plugin.mlpack +src/good_plugin.mlpack +theories/evil.v +theories/good.v diff --git a/test-suite/misc/non-marshalable-state/src/evil.mlg b/test-suite/misc/non-marshalable-state/src/evil.mlg new file mode 100644 index 0000000000..59b2b5a8ac --- /dev/null +++ b/test-suite/misc/non-marshalable-state/src/evil.mlg @@ -0,0 +1,15 @@ +DECLARE PLUGIN "evil_plugin" + +{ + +let state = Summary.ref + ~name:"elpi-compiler-cache" + None + +} + +VERNAC COMMAND EXTEND magic CLASSIFIED AS SIDEFF +| [ "magic" ] -> { + state := Some (fun () -> ()) +} +END diff --git a/test-suite/misc/non-marshalable-state/src/evil_plugin.mlpack b/test-suite/misc/non-marshalable-state/src/evil_plugin.mlpack new file mode 100644 index 0000000000..6382aa69e1 --- /dev/null +++ b/test-suite/misc/non-marshalable-state/src/evil_plugin.mlpack @@ -0,0 +1 @@ +Evil diff --git a/test-suite/misc/non-marshalable-state/src/good.mlg b/test-suite/misc/non-marshalable-state/src/good.mlg new file mode 100644 index 0000000000..c6b9cbefd5 --- /dev/null +++ b/test-suite/misc/non-marshalable-state/src/good.mlg @@ -0,0 +1,16 @@ +DECLARE PLUGIN "good_plugin" + +{ + +let state = Summary.Local.ref + ~name:"elpi-compiler-cache" + None + +} + +VERNAC COMMAND EXTEND magic CLASSIFIED AS SIDEFF +| [ "magic" ] -> { + let open Summary.Local in + state := Some (fun () -> ()) +} +END diff --git a/test-suite/misc/non-marshalable-state/src/good_plugin.mlpack b/test-suite/misc/non-marshalable-state/src/good_plugin.mlpack new file mode 100644 index 0000000000..cd9dd73b78 --- /dev/null +++ b/test-suite/misc/non-marshalable-state/src/good_plugin.mlpack @@ -0,0 +1 @@ +Good diff --git a/test-suite/misc/non-marshalable-state/theories/evil.v b/test-suite/misc/non-marshalable-state/theories/evil.v new file mode 100644 index 0000000000..661482a975 --- /dev/null +++ b/test-suite/misc/non-marshalable-state/theories/evil.v @@ -0,0 +1,5 @@ +Declare ML Module "evil_plugin". + +magic. + +Lemma x : True. Proof. trivial. Qed. diff --git a/test-suite/misc/non-marshalable-state/theories/good.v b/test-suite/misc/non-marshalable-state/theories/good.v new file mode 100644 index 0000000000..eab9a043e1 --- /dev/null +++ b/test-suite/misc/non-marshalable-state/theories/good.v @@ -0,0 +1,5 @@ +Declare ML Module "good_plugin". + +magic. + +Lemma x : True. Proof. trivial. Qed. diff --git a/test-suite/output-coqtop/DependentEvars.out b/test-suite/output-coqtop/DependentEvars.out index 2e69b94505..11d1ca0bdb 100644 --- a/test-suite/output-coqtop/DependentEvars.out +++ b/test-suite/output-coqtop/DependentEvars.out @@ -1,6 +1,6 @@ Coq < -Coq < Coq < 1 subgoal +Coq < Coq < 1 goal ============================ forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R @@ -8,12 +8,12 @@ Coq < Coq < 1 subgoal (dependent evars: ; in current goal:) strange_imp_trans < -strange_imp_trans < No more subgoals. +strange_imp_trans < No more goals. (dependent evars: ; in current goal:) strange_imp_trans < -Coq < Coq < 1 subgoal +Coq < Coq < 1 goal ============================ forall P Q : Prop, (P -> Q) /\ P -> Q @@ -21,7 +21,7 @@ Coq < Coq < 1 subgoal (dependent evars: ; in current goal:) modpon < -modpon < No more subgoals. +modpon < No more goals. (dependent evars: ; in current goal:) @@ -38,7 +38,7 @@ Coq < p123 is declared Coq < p34 is declared -Coq < Coq < 1 subgoal +Coq < Coq < 1 goal P1, P2, P3, P4 : Prop p12 : P1 -> P2 @@ -50,7 +50,7 @@ Coq < Coq < 1 subgoal (dependent evars: ; in current goal:) p14 < -p14 < 4 focused subgoals +p14 < 4 focused goals (shelved: 2) P1, P2, P3, P4 : Prop @@ -60,16 +60,16 @@ p14 < 4 focused subgoals ============================ ?Q -> P4 -subgoal 2 is: +goal 2 is: ?P -> ?Q -subgoal 3 is: +goal 3 is: ?P -> ?Q -subgoal 4 is: +goal 4 is: ?P (dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5) -p14 < 3 focused subgoals +p14 < 3 focused goals (shelved: 2) P1, P2, P3, P4 : Prop @@ -79,9 +79,9 @@ p14 < 3 focused subgoals ============================ ?P -> (?P0 -> P4) /\ ?P0 -subgoal 2 is: +goal 2 is: ?P -> (?P0 -> P4) /\ ?P0 -subgoal 3 is: +goal 3 is: ?P (dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?P0; in current goal: ?X4 ?X5 ?X10 ?X11) diff --git a/test-suite/output-coqtop/DependentEvars2.out b/test-suite/output-coqtop/DependentEvars2.out index 63bfafa88d..6bf2c35ad4 100644 --- a/test-suite/output-coqtop/DependentEvars2.out +++ b/test-suite/output-coqtop/DependentEvars2.out @@ -1,6 +1,6 @@ Coq < -Coq < Coq < 1 subgoal +Coq < Coq < 1 goal ============================ forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R @@ -8,12 +8,12 @@ Coq < Coq < 1 subgoal (dependent evars: ; in current goal:) strange_imp_trans < -strange_imp_trans < No more subgoals. +strange_imp_trans < No more goals. (dependent evars: ; in current goal:) strange_imp_trans < -Coq < Coq < 1 subgoal +Coq < Coq < 1 goal ============================ forall P Q : Prop, (P -> Q) /\ P -> Q @@ -21,7 +21,7 @@ Coq < Coq < 1 subgoal (dependent evars: ; in current goal:) modpon < -modpon < No more subgoals. +modpon < No more goals. (dependent evars: ; in current goal:) @@ -38,7 +38,7 @@ Coq < p123 is declared Coq < p34 is declared -Coq < Coq < 1 subgoal +Coq < Coq < 1 goal P1, P2, P3, P4 : Prop p12 : P1 -> P2 @@ -52,7 +52,7 @@ Coq < Coq < 1 subgoal p14 < p14 < Second proof: -p14 < 4 focused subgoals +p14 < 4 focused goals (shelved: 2) P1, P2, P3, P4 : Prop @@ -62,16 +62,16 @@ p14 < 4 focused subgoals ============================ ?Q -> P4 -subgoal 2 is: +goal 2 is: ?P -> ?Q -subgoal 3 is: +goal 3 is: ?P -> ?Q -subgoal 4 is: +goal 4 is: ?P (dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5) -p14 < 1 focused subgoal +p14 < 1 focused goal (shelved: 2) P1, P2, P3, P4 : Prop @@ -86,19 +86,19 @@ p14 < 1 focused subgoal p14 < This subproof is complete, but there are some unfocused goals. Try unfocusing with "}". -3 subgoals +3 goals (shelved: 2) -subgoal 1 is: +goal 1 is: ?P -> (?P0 -> P4) /\ ?P0 -subgoal 2 is: +goal 2 is: ?P -> (?P0 -> P4) /\ ?P0 -subgoal 3 is: +goal 3 is: ?P (dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?P0; in current goal:) -p14 < 3 focused subgoals +p14 < 3 focused goals (shelved: 2) P1, P2, P3, P4 : Prop @@ -108,9 +108,9 @@ p14 < 3 focused subgoals ============================ ?P -> (?P0 -> P4) /\ ?P0 -subgoal 2 is: +goal 2 is: ?P -> (?P0 -> P4) /\ ?P0 -subgoal 3 is: +goal 3 is: ?P (dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?P0; in current goal: ?X4 ?X5 ?X10 ?X11) diff --git a/test-suite/output-coqtop/ShowGoal.out b/test-suite/output-coqtop/ShowGoal.out index 42d9ff31e9..467112f153 100644 --- a/test-suite/output-coqtop/ShowGoal.out +++ b/test-suite/output-coqtop/ShowGoal.out @@ -1,52 +1,52 @@ -Coq < 1 subgoal
+Coq < 1 goal
============================
forall i : nat, exists j k : nat, i = j /\ j = k /\ i = k
x <
-x < 1 focused subgoal
+x < 1 focused goal
(shelved: 1)
i : nat
============================
exists k : nat, i = ?j /\ ?j = k /\ i = k
-x < 1 focused subgoal
+x < 1 focused goal
(shelved: 2)
i : nat
============================
i = ?j /\ ?j = ?k /\ i = ?k
-x < 2 focused subgoals
+x < 2 focused goals
(shelved: 2)
i : nat
============================
i = ?j
-subgoal 2 is:
+goal 2 is:
?j = ?k /\ i = ?k
-x < 1 focused subgoal
+x < 1 focused goal
(shelved: 1)
i : nat
============================
i = ?k /\ i = ?k
-x < 2 focused subgoals
+x < 2 focused goals
(shelved: 1)
i : nat
============================
i = ?k
-subgoal 2 is:
+goal 2 is:
i = ?k
-x < 1 subgoal
+x < 1 goal
i : nat
============================
diff --git a/test-suite/output-coqtop/ShowProofDiffs.out b/test-suite/output-coqtop/ShowProofDiffs.out index 285a3bcd89..a37e3e5af4 100644 --- a/test-suite/output-coqtop/ShowProofDiffs.out +++ b/test-suite/output-coqtop/ShowProofDiffs.out @@ -1,11 +1,11 @@ -Coq < Coq < 1 subgoal
+Coq < Coq < 1 goal
============================
[48;2;0;91;0m[48;2;0;141;0;4m[1mforall[22m i : nat, [37mexists[39m j k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k[48;2;0;91;0;24m[0m
x <
-x < 1 focused subgoal
+x < 1 focused goal
(shelved: 1)
[48;2;0;91;0m[48;2;0;141;0;4mi : nat[48;2;0;91;0;24m[0m
============================
@@ -14,7 +14,7 @@ x < 1 focused subgoal [48;2;0;91;0m[48;2;0;141;0;4m([1mfun[22m i : nat =>[49;24m
[48;2;0;141;0;4mex_intro ([1mfun[22m j : nat => [37mexists[39m k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k) [94m?[39m[94mj[39m[48;2;0;91;0;24m ?Goal[48;2;0;141;0;4m)[48;2;0;91;0;24m[0m
-x < 1 focused subgoal
+x < 1 focused goal
(shelved: 2)
i : nat
============================
@@ -24,13 +24,13 @@ x < 1 focused subgoal [48;2;0;91;0mex_intro ([1mfun[22m j : nat => [37mexists[39m k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k) [49m
[48;2;0;91;0m[48;2;0;141;0;4m[94m?[39m[94mj[39m (ex_intro ([1mfun[22m k : nat => i[37m =[39m ?j[37m /\[39m[48;2;0;91;0;24m ?j[37m [39m[48;2;0;141;0;4m[37m=[39m k[37m /\[39m i[37m =[39m k) [94m?[39m[94mk[39m[48;2;0;91;0;24m ?Goal[48;2;0;141;0;4m)[48;2;0;91;0;24m)[0m
-x < 2 focused subgoals
+x < 2 focused goals
(shelved: 2)
i : nat
============================
[48;2;0;91;0mi[37m =[39m ?j[0m
-subgoal 2 is:
+goal 2 is:
[48;2;0;91;0m?j[37m =[39m ?k[37m /\[39m i[37m =[39m ?k[0m
[48;2;0;91;0m([1mfun[22m i : nat =>[49m
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index e46774f68a..9fd846ac16 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -11,7 +11,7 @@ eq_refl : ?y = ?y where ?y : [ |- nat] -Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x +Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x. Arguments eq {A}%type_scope _ _ Arguments eq_refl {B}%type_scope {y}, [_] _ @@ -22,7 +22,7 @@ eq_refl is not universe polymorphic Arguments eq_refl {B}%type_scope {y}, [_] _ (where some original arguments have been renamed) Expands to: Constructor Coq.Init.Logic.eq_refl -Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x +Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x. Arguments myEq _%type_scope _ _ Arguments myrefl {C}%type_scope x _ @@ -55,7 +55,7 @@ Expands to: Constant Arguments_renaming.Test1.myplus @myplus : forall Z : Type, Z -> nat -> nat -> nat Inductive myEq (A B : Type) (x : A) : A -> Prop := - myrefl : B -> myEq A B x x + myrefl : B -> myEq A B x x. Arguments myEq (_ _)%type_scope _ _ Arguments myrefl A%type_scope {C}%type_scope x _ diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 6fd4d37ab4..ea647a990a 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -89,7 +89,7 @@ Arguments lem2 _%bool_scope lem3 = fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl : forall k : nat * nat, k = k -1 subgoal +1 goal x : nat n, n0 := match x + 0 with @@ -109,7 +109,7 @@ fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl end : x = x ============================ x + 0 = 0 -1 subgoal +1 goal p : nat a, diff --git a/test-suite/output/CompactContexts.out b/test-suite/output/CompactContexts.out index 9d1d19877e..f0a8019b67 100644 --- a/test-suite/output/CompactContexts.out +++ b/test-suite/output/CompactContexts.out @@ -1,4 +1,4 @@ -1 subgoal +1 goal hP1 : True a : nat b : list nat h : forall x : nat, {y : nat | y > x} diff --git a/test-suite/output/Function.out b/test-suite/output/Function.out new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/test-suite/output/Function.out diff --git a/test-suite/output/Function.v b/test-suite/output/Function.v new file mode 100644 index 0000000000..b3e2a93895 --- /dev/null +++ b/test-suite/output/Function.v @@ -0,0 +1,31 @@ +Require Import FunInd List. + +(* Explanations: This kind of pattern matching displays a legitimate + unused variable warning in v8.13. + +Fixpoint f (l:list nat) : nat := + match l with + | nil => O + | S n :: nil => 1 + | x :: l' => f l' + end. +*) + +(* In v8.13 the same code with "Function" generates a lot more + warnings about variables created automatically by Function. These + are not legitimate. PR #13776 (post v8.13) removes all warnings + about pattern matching variables (and non truly recursive fixpoint) + for "Function". So this should not generate any warning. Note that + this PR removes also the legitimate warnings. It would be better if + this test generate the same warning as the Fixpoint above. This + test would then need to be updated. *) + +(* Ensuring the warning is a warning. *) +Set Warnings "matching-variable". +(* But no warning generated here. *) +Function f (l:list nat) : nat := + match l with + | nil => O + | S n :: nil => 1 + | n :: l' => f l' + end. diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out index 8e10107673..fc3b6fbd99 100644 --- a/test-suite/output/Inductive.out +++ b/test-suite/output/Inductive.out @@ -5,7 +5,7 @@ A : Set a : A l : list' A Unable to unify "list' (A * A)%type" with "list' A". -Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x +Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x. Arguments foo _%type_scope _ Arguments Foo _%type_scope _ diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out index 02e58775b5..fdd609f5b2 100644 --- a/test-suite/output/InitSyntax.out +++ b/test-suite/output/InitSyntax.out @@ -1,5 +1,5 @@ Inductive sig2 (A : Type) (P Q : A -> Prop) : Type := - exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x} + exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x}. Arguments sig2 [A]%type_scope (_ _)%type_scope Arguments exist2 [A]%type_scope (_ _)%function_scope _ _ _ diff --git a/test-suite/output/Int63Syntax.out b/test-suite/output/Int63Syntax.out index ca8e1b58a8..7ca4de1e46 100644 --- a/test-suite/output/Int63Syntax.out +++ b/test-suite/output/Int63Syntax.out @@ -56,3 +56,21 @@ t = 2%i63 : int = 37151199385380486 : int + = 4 + : int + = 4 + : int + = 4 + : int + = add + : int -> int -> int + = 12 + : int + = 12 + : int + = 12 + : int + = 3 + x + : int + = 1 + 2 + x + : int diff --git a/test-suite/output/Int63Syntax.v b/test-suite/output/Int63Syntax.v index 6f1046f7a5..50910264f2 100644 --- a/test-suite/output/Int63Syntax.v +++ b/test-suite/output/Int63Syntax.v @@ -40,3 +40,18 @@ Open Scope int63_scope. Check (2+2). Eval vm_compute in 2+2. Eval vm_compute in 65675757 * 565675998. + +Eval simpl in 2+2. +Eval hnf in 2+2. +Eval cbn in 2+2. +Eval hnf in PrimInt63.add. + +Eval simpl in (2 * 3) + (2 * 3). +Eval hnf in (2 * 3) + (2 * 3). +Eval cbn in (2 * 3) + (2 * 3). + +Section TestNoSimpl. +Variable x : int. +Eval simpl in 1 + 2 + x. +Eval hnf in 1 + 2 + x. +End TestNoSimpl. diff --git a/test-suite/output/Intuition.out b/test-suite/output/Intuition.out index f2bf25ca65..e273307d75 100644 --- a/test-suite/output/Intuition.out +++ b/test-suite/output/Intuition.out @@ -1,4 +1,4 @@ -1 subgoal +1 goal m, n : Z H : (m >= n)%Z diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out index 0a989646cf..2daa5a6bb5 100644 --- a/test-suite/output/Naming.out +++ b/test-suite/output/Naming.out @@ -1,23 +1,23 @@ -1 subgoal +1 goal x3 : nat ============================ forall x x1 x4 x0 : nat, (forall x2 x5 : nat, x2 + x1 = x4 + x5) -> x + x1 = x4 + x0 -1 subgoal +1 goal x3, x, x1, x4, x0 : nat H : forall x x3 : nat, x + x1 = x4 + x3 ============================ x + x1 = x4 + x0 -1 subgoal +1 goal 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) -1 subgoal +1 goal x3 : nat ============================ @@ -27,7 +27,7 @@ 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 +1 goal x3, x, x1, x4, x0 : nat ============================ @@ -36,7 +36,7 @@ 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 +1 goal x3, x, x1, x4, x0 : nat H : forall x x3 : nat, @@ -45,7 +45,7 @@ H0 : x + x1 = x4 + x0 ============================ forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x -1 subgoal +1 goal x3, x, x1, x4, x0 : nat H : forall x x3 : nat, @@ -55,7 +55,7 @@ x5, x6, x7, S : nat ============================ x5 + S = x6 + x7 + Datatypes.S x -1 subgoal +1 goal x3, a : nat H : a = 0 -> forall a : nat, a = 0 diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index a9bed49922..60213cab0c 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -238,7 +238,7 @@ Notation "'exists' ! x .. y , p" := (default interpretation) Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope (default interpretation) -1 subgoal +1 goal ============================ ##@% diff --git a/test-suite/output/Partac.out b/test-suite/output/Partac.out index 889e698fa2..ce5dbdedb4 100644 --- a/test-suite/output/Partac.out +++ b/test-suite/output/Partac.out @@ -1,6 +1,6 @@ The command has indeed failed with message: The term "false" has type "bool" while it is expected to have type "nat". -(for subgoal 1) +(for goal 1) The command has indeed failed with message: The term "0" has type "nat" while it is expected to have type "bool". -(for subgoal 2) +(for goal 2) diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index fe16dba496..03b9e3b527 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -4,14 +4,14 @@ existT is template universe polymorphic on sigT.u0 sigT.u1 Arguments existT [A]%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} + existT : forall x : A, P x -> {x : A & P x}. Arguments sigT [A]%type_scope _%type_scope Arguments existT [A]%type_scope _%function_scope _ _ existT : forall [A : Type] (P : A -> Type) (x : A), P x -> {x : A & P x} Argument A is implicit -Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x +Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x. Arguments eq {A}%type_scope _ _ Arguments eq_refl {A}%type_scope {x}, [_] _ @@ -50,7 +50,7 @@ Arguments plus_n_O _%nat_scope plus_n_O is opaque Expands to: Constant Coq.Init.Peano.plus_n_O Inductive le (n : nat) : nat -> Prop := - le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m + le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m. Arguments le (_ _)%nat_scope Arguments le_n _%nat_scope @@ -60,7 +60,7 @@ comparison : Set comparison is not universe polymorphic Expands to: Inductive Coq.Init.Datatypes.comparison Inductive comparison : Set := - Eq : comparison | Lt : comparison | Gt : comparison + Eq : comparison | Lt : comparison | Gt : comparison. bar : foo bar is not universe polymorphic @@ -78,7 +78,7 @@ Arguments bar {x} Module Coq.Init.Peano Notation sym_eq := eq_sym Expands to: Notation Coq.Init.Logic.sym_eq -Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x +Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x. Arguments eq {A}%type_scope _ _ Arguments eq_refl {A}%type_scope {x}, {_} _ diff --git a/test-suite/output/PrintModule.out b/test-suite/output/PrintModule.out index 1a9bc068c5..7c7600b786 100644 --- a/test-suite/output/PrintModule.out +++ b/test-suite/output/PrintModule.out @@ -7,3 +7,11 @@ Module N : S with Module T := K := M Module N : S with Module T := M Module Type Func = Funsig (T0:Test) Sig Parameter x : T0.t. End +Module +A +:= Struct + Variant I : Set := C : nat -> I. + Record R : Set := Build_R { n : nat }. + Definition n : R -> nat. + End + diff --git a/test-suite/output/PrintModule.v b/test-suite/output/PrintModule.v index 54ef305be4..b4de03b556 100644 --- a/test-suite/output/PrintModule.v +++ b/test-suite/output/PrintModule.v @@ -60,3 +60,10 @@ Print Func. End Shortest_path. End QUX. + +Module A. +Variant I := C : nat -> I. +Record R := { n : nat }. +End A. + +Print Module A. diff --git a/test-suite/output/SearchHead.v b/test-suite/output/SearchHead.v deleted file mode 100644 index 2ee8a0d184..0000000000 --- a/test-suite/output/SearchHead.v +++ /dev/null @@ -1,19 +0,0 @@ -(* Some tests of the Search command *) - -SearchHead le. (* app nodes *) -SearchHead bool. (* no apps *) -SearchHead (@eq nat). (* complex pattern *) - -Definition newdef := fun x:nat => x = x. - -Goal forall n:nat, newdef n -> False. - intros n h. - SearchHead newdef. (* search hypothesis *) -Abort. - - -Goal forall n (P:nat -> Prop), P n -> False. - intros n P h. - SearchHead P. (* search hypothesis also for patterns *) -Abort. - diff --git a/test-suite/output/SearchHead.out b/test-suite/output/Search_headconcl.out index 2f0d854ac6..24e2ee76af 100644 --- a/test-suite/output/SearchHead.out +++ b/test-suite/output/Search_headconcl.out @@ -1,17 +1,9 @@ -File "stdin", line 3, characters 0-14: -Warning: -SearchHead is deprecated. Use the headconcl: clause of Search instead. -[deprecated-searchhead,deprecated] le_n: forall n : nat, n <= n le_0_n: forall n : nat, 0 <= n le_S: forall n m : nat, n <= m -> n <= S m le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m le_n_S: forall n m : nat, n <= m -> S n <= S m le_S_n: forall n m : nat, S n <= S m -> n <= m -File "stdin", line 4, characters 0-16: -Warning: -SearchHead is deprecated. Use the headconcl: clause of Search instead. -[deprecated-searchhead,deprecated] false: bool true: bool negb: bool -> bool @@ -35,10 +27,6 @@ Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool Decimal.int_beq: Decimal.int -> Decimal.int -> bool Decimal.uint_beq: Decimal.uint -> Decimal.uint -> bool -File "stdin", line 5, characters 0-21: -Warning: -SearchHead is deprecated. Use the headconcl: clause of Search instead. -[deprecated-searchhead,deprecated] mult_n_O: forall n : nat, 0 = n * 0 plus_O_n: forall n : nat, 0 + n = n plus_n_O: forall n : nat, n = n + 0 @@ -57,13 +45,5 @@ f_equal2_plus: forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2 f_equal2_mult: forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2 -File "stdin", line 11, characters 2-20: -Warning: -SearchHead is deprecated. Use the headconcl: clause of Search instead. -[deprecated-searchhead,deprecated] h: newdef n -File "stdin", line 17, characters 2-15: -Warning: -SearchHead is deprecated. Use the headconcl: clause of Search instead. -[deprecated-searchhead,deprecated] h: P n diff --git a/test-suite/output/Search_headconcl.v b/test-suite/output/Search_headconcl.v new file mode 100644 index 0000000000..8b168dcd25 --- /dev/null +++ b/test-suite/output/Search_headconcl.v @@ -0,0 +1,18 @@ +(* Some tests of the Search command *) + +Search headconcl: le. (* app nodes *) +Search headconcl: bool. (* no apps *) +Search headconcl: (@eq nat). (* complex pattern *) + +Definition newdef := fun x:nat => x = x. + +Goal forall n:nat, newdef n -> False. + intros n h. + Search headconcl: newdef. (* search hypothesis *) +Abort. + + +Goal forall n (P:nat -> Prop), P n -> False. + intros n P h. + Search headconcl: P. (* search hypothesis also for patterns *) +Abort. diff --git a/test-suite/output/Show.out b/test-suite/output/Show.out index f02e442be5..3db00be048 100644 --- a/test-suite/output/Show.out +++ b/test-suite/output/Show.out @@ -1,10 +1,10 @@ -3 subgoals (ID 29) +3 goals (ID 29) H : 0 = 0 ============================ 1 = 1 -subgoal 2 (ID 33) is: +goal 2 (ID 33) is: 1 = S (S m') -subgoal 3 (ID 20) is: +goal 3 (ID 20) is: S (S n') = S m diff --git a/test-suite/output/Unicode.out b/test-suite/output/Unicode.out index a57b3bbad5..abe6c39e8f 100644 --- a/test-suite/output/Unicode.out +++ b/test-suite/output/Unicode.out @@ -1,4 +1,4 @@ -1 subgoal +1 goal very_very_long_type_name1 : Type very_very_long_type_name2 : Type @@ -8,7 +8,7 @@ → True → ∀ (x : very_very_long_type_name1) (y : very_very_long_type_name2), f x y ∧ f x y ∧ f x y ∧ f x y ∧ f x y ∧ f x y -1 subgoal +1 goal very_very_long_type_name1 : Type very_very_long_type_name2 : Type @@ -18,7 +18,7 @@ → True → ∀ (x : very_very_long_type_name2) (y : very_very_long_type_name1) (z : very_very_long_type_name2), f y x ∧ f y z -1 subgoal +1 goal very_very_long_type_name1 : Type very_very_long_type_name2 : Type @@ -29,7 +29,7 @@ → ∀ (x : very_very_long_type_name2) (y : very_very_long_type_name1) (z : very_very_long_type_name2), f y x ∧ f y z ∧ f y x ∧ f y z ∧ f y x ∧ f y z -1 subgoal +1 goal very_very_long_type_name1 : Type very_very_long_type_name2 : Type diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 95b6c6ee95..4993b747fa 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -1,6 +1,7 @@ -Inductive Empty@{uu} : Type@{uu} := +Inductive Empty@{uu} : Type@{uu} := . (* uu |= *) -Record PWrap (A : Type@{uu}) : Type@{uu} := pwrap { punwrap : A } +Record PWrap (A : Type@{uu}) : Type@{uu} := pwrap + { punwrap : A }. (* uu |= *) PWrap has primitive projections with eta conversion. @@ -12,7 +13,8 @@ fun (A : Type@{uu}) (p : PWrap@{uu} A) => punwrap _ p (* uu |= *) Arguments punwrap _%type_scope _ -Record RWrap (A : Type@{uu}) : Type@{uu} := rwrap { runwrap : A } +Record RWrap (A : Type@{uu}) : Type@{uu} := rwrap + { runwrap : A }. (* uu |= *) Arguments RWrap _%type_scope @@ -80,9 +82,9 @@ foo@{uu u v} = Type@{u} -> Type@{v} -> Type@{uu} : Type@{max(uu+1,u+1,v+1)} (* uu u v |= *) -Inductive Empty@{E} : Type@{E} := +Inductive Empty@{E} : Type@{E} := . (* E |= *) -Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A } +Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }. (* E |= *) PWrap has primitive projections with eta conversion. @@ -107,7 +109,7 @@ insec@{v} = Type@{uu} -> Type@{v} : Type@{max(uu+1,v+1)} (* v |= *) Inductive insecind@{k} : Type@{k+1} := - inseccstr : Type@{k} -> insecind@{k} + inseccstr : Type@{k} -> insecind@{k}. (* k |= *) Arguments inseccstr _%type_scope @@ -115,7 +117,7 @@ insec@{uu v} = Type@{uu} -> Type@{v} : Type@{max(uu+1,v+1)} (* uu v |= *) Inductive insecind@{uu k} : Type@{k+1} := - inseccstr : Type@{k} -> insecind@{uu k} + inseccstr : Type@{k} -> insecind@{uu k}. (* uu k |= *) Arguments inseccstr _%type_scope diff --git a/test-suite/output/bug_13821_native_command_line_warn.out b/test-suite/output/bug_13821_native_command_line_warn.out new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/test-suite/output/bug_13821_native_command_line_warn.out diff --git a/test-suite/output/bug_13821_native_command_line_warn.v b/test-suite/output/bug_13821_native_command_line_warn.v new file mode 100644 index 0000000000..a28210b6c2 --- /dev/null +++ b/test-suite/output/bug_13821_native_command_line_warn.v @@ -0,0 +1 @@ +(* -*- coq-prog-args: ("-w" "-native-compiler-disabled" "-native-compiler" "ondemand"); -*- *) diff --git a/test-suite/output/bug_9370.out b/test-suite/output/bug_9370.out index 0ff151c8b4..8d34b7143a 100644 --- a/test-suite/output/bug_9370.out +++ b/test-suite/output/bug_9370.out @@ -1,12 +1,12 @@ -1 subgoal +1 goal ============================ 1 = 1 -1 subgoal +1 goal ============================ 1 = 1 -1 subgoal +1 goal ============================ 1 = 1 diff --git a/test-suite/output/bug_9403.out b/test-suite/output/bug_9403.out index 850760d5ed..cd1030bd2e 100644 --- a/test-suite/output/bug_9403.out +++ b/test-suite/output/bug_9403.out @@ -1,4 +1,4 @@ -1 subgoal +1 goal X : tele α, β, γ1, γ2 : X → Prop diff --git a/test-suite/output/bug_9569.out b/test-suite/output/bug_9569.out index 2d474e4933..e49449679f 100644 --- a/test-suite/output/bug_9569.out +++ b/test-suite/output/bug_9569.out @@ -1,16 +1,16 @@ -1 subgoal +1 goal ============================ exists I : True, I = Logic.I -1 subgoal +1 goal ============================ f True False True False (Logic.True /\ Logic.False) -1 subgoal +1 goal ============================ [I | I = Logic.I; I = Logic.I] = [I | I = Logic.I; I = Logic.I] -1 subgoal +1 goal ============================ [I & I = Logic.I | I = Logic.I; Logic.I = I] diff --git a/test-suite/output/clear.out b/test-suite/output/clear.out index 42e3abf26f..ea01ac50d7 100644 --- a/test-suite/output/clear.out +++ b/test-suite/output/clear.out @@ -1,4 +1,4 @@ -1 subgoal +1 goal z := 0 : nat ============================ diff --git a/test-suite/output/goal_output.out b/test-suite/output/goal_output.out index 17c1aaa55b..453f6ee615 100644 --- a/test-suite/output/goal_output.out +++ b/test-suite/output/goal_output.out @@ -2,79 +2,79 @@ Nat.t = nat : Set Nat.t = nat : Set -2 subgoals +2 goals ============================ True -subgoal 2 is: +goal 2 is: True -2 subgoals, subgoal 1 (?Goal) +2 goals, goal 1 (?Goal) ============================ True -subgoal 2 (?Goal0) is: +goal 2 (?Goal0) is: True -1 subgoal +1 goal ============================ True -1 subgoal (?Goal0) +1 goal (?Goal0) ============================ True -1 subgoal (?Goal0) +1 goal (?Goal0) ============================ True *** Unfocused goals: -subgoal 2 (?Goal1) is: +goal 2 (?Goal1) is: True -subgoal 3 (?Goal) is: +goal 3 (?Goal) is: True -1 subgoal +1 goal ============================ True *** Unfocused goals: -subgoal 2 is: +goal 2 is: True -subgoal 3 is: +goal 3 is: True This subproof is complete, but there are some unfocused goals. Focus next goal with bullet -. -2 subgoals +2 goals -subgoal 1 is: +goal 1 is: True -subgoal 2 is: +goal 2 is: True This subproof is complete, but there are some unfocused goals. Focus next goal with bullet -. -2 subgoals +2 goals -subgoal 1 (?Goal0) is: +goal 1 (?Goal0) is: True -subgoal 2 (?Goal) is: +goal 2 (?Goal) is: True This subproof is complete, but there are some unfocused goals. Focus next goal with bullet -. -1 subgoal +1 goal -subgoal 1 is: +goal 1 is: True This subproof is complete, but there are some unfocused goals. Focus next goal with bullet -. -1 subgoal +1 goal -subgoal 1 (?Goal) is: +goal 1 (?Goal) is: True diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index efdc94fb1e..ed42429f85 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -38,7 +38,7 @@ Ltac foo := let w := () in let z := 1 in pose v -2 subgoals +2 goals n : nat ============================ @@ -47,5 +47,5 @@ Ltac foo := | S n1 => a n1 end) n = n -subgoal 2 is: +goal 2 is: forall a : nat, a = 0 diff --git a/test-suite/output/names.out b/test-suite/output/names.out index 48be63a46a..051bce7701 100644 --- a/test-suite/output/names.out +++ b/test-suite/output/names.out @@ -3,7 +3,7 @@ In environment y : nat The term "a y" has type "{y0 : nat | y = y0}" while it is expected to have type "{x : nat | x = y}". -1 focused subgoal +1 focused goal (shelved: 1) H : ?n <= 3 -> 3 <= ?n -> ?n = 3 diff --git a/test-suite/output/optimize_heap.out b/test-suite/output/optimize_heap.out index 94a0b19118..b6ee61a971 100644 --- a/test-suite/output/optimize_heap.out +++ b/test-suite/output/optimize_heap.out @@ -1,8 +1,8 @@ -1 subgoal +1 goal ============================ True -1 subgoal +1 goal ============================ True diff --git a/test-suite/output/set.out b/test-suite/output/set.out index 4b72d73eb3..61f3c52656 100644 --- a/test-suite/output/set.out +++ b/test-suite/output/set.out @@ -1,16 +1,16 @@ -1 subgoal +1 goal y1 := 0 : nat x := 0 + 0 : nat ============================ x = x -1 subgoal +1 goal y1, y2 := 0 : nat x := y2 + 0 : nat ============================ x = x -1 subgoal +1 goal y1, y2, y3 := 0 : nat x := y2 + y3 : nat diff --git a/test-suite/output/simpl.out b/test-suite/output/simpl.out index 526e468f5b..fd35c5e339 100644 --- a/test-suite/output/simpl.out +++ b/test-suite/output/simpl.out @@ -1,14 +1,14 @@ -1 subgoal +1 goal x : nat ============================ x = S x -1 subgoal +1 goal x : nat ============================ 0 + x = S x -1 subgoal +1 goal x : nat ============================ diff --git a/test-suite/output/subst.out b/test-suite/output/subst.out index 209b2bc26f..9cc515b7ba 100644 --- a/test-suite/output/subst.out +++ b/test-suite/output/subst.out @@ -1,4 +1,4 @@ -1 subgoal +1 goal y, z : nat Hy : y = 0 @@ -11,7 +11,7 @@ H4 : z = 4 ============================ True -1 subgoal +1 goal x, z : nat Hx : x = 0 @@ -24,7 +24,7 @@ H4 : z = 4 ============================ True -1 subgoal +1 goal x, y : nat Hx : x = 0 @@ -37,7 +37,7 @@ H4 : 0 = 4 ============================ True -1 subgoal +1 goal H1 : 0 = 1 HA : True @@ -47,7 +47,7 @@ H4 : 0 = 4 ============================ True -1 subgoal +1 goal y, z : nat Hy : y = 0 @@ -60,7 +60,7 @@ H2 : 0 = 2 ============================ True -1 subgoal +1 goal x, z : nat Hx : x = 0 @@ -73,7 +73,7 @@ H3 : 0 = 3 ============================ True -1 subgoal +1 goal x, y : nat Hx : x = 0 @@ -86,7 +86,7 @@ H4 : 0 = 4 ============================ True -1 subgoal +1 goal HA, HB : True H4 : 0 = 4 diff --git a/test-suite/output/unifconstraints.out b/test-suite/output/unifconstraints.out index 2fadd747b7..abcb8d7e0c 100644 --- a/test-suite/output/unifconstraints.out +++ b/test-suite/output/unifconstraints.out @@ -1,44 +1,44 @@ -3 focused subgoals +3 focused goals (shelved: 1) ============================ ?Goal 0 -subgoal 2 is: +goal 2 is: forall n : nat, ?Goal n -> ?Goal (S n) -subgoal 3 is: +goal 3 is: nat unification constraint: ?Goal ?Goal2 <= True /\ True /\ True \/ veeryyyyyyyyyyyyloooooooooooooonggidentifier = veeryyyyyyyyyyyyloooooooooooooonggidentifier -3 focused subgoals +3 focused goals (shelved: 1) n, m : nat ============================ ?Goal@{n:=n; m:=m} 0 -subgoal 2 is: +goal 2 is: forall n0 : nat, ?Goal@{n:=n; m:=m} n0 -> ?Goal@{n:=n; m:=m} (S n0) -subgoal 3 is: +goal 3 is: nat unification constraint: ?Goal@{n:=n; m:=m} ?Goal2@{n:=n; m:=m} <= True /\ True /\ True \/ veeryyyyyyyyyyyyloooooooooooooonggidentifier = veeryyyyyyyyyyyyloooooooooooooonggidentifier -3 focused subgoals +3 focused goals (shelved: 1) m : nat ============================ ?Goal1@{m:=m} 0 -subgoal 2 is: +goal 2 is: forall n0 : nat, ?Goal1@{m:=m} n0 -> ?Goal1@{m:=m} (S n0) -subgoal 3 is: +goal 3 is: nat unification constraint: @@ -46,16 +46,16 @@ unification constraint: True /\ True /\ True \/ veeryyyyyyyyyyyyloooooooooooooonggidentifier = veeryyyyyyyyyyyyloooooooooooooonggidentifier -3 focused subgoals +3 focused goals (shelved: 1) m : nat ============================ ?Goal0@{m:=m} 0 -subgoal 2 is: +goal 2 is: forall n0 : nat, ?Goal0@{m:=m} n0 -> ?Goal0@{m:=m} (S n0) -subgoal 3 is: +goal 3 is: nat unification constraint: diff --git a/test-suite/output/unification.out b/test-suite/output/unification.out index cf31871e5a..4db5c2d161 100644 --- a/test-suite/output/unification.out +++ b/test-suite/output/unification.out @@ -9,25 +9,25 @@ Unable to unify "T" with "?X@{x0:=x; x:=C a}" (cannot instantiate The command has indeed failed with message: The term "id" has type "ID" while it is expected to have type "Type -> ?T" (cannot instantiate "?T" because "A" is not in its scope). -1 focused subgoal +1 focused goal (shelved: 1) H : forall x : nat, S (S (S x)) = x ============================ ?x = 0 -1 focused subgoal +1 focused goal (shelved: 1) H : forall x : nat, S (S (S x)) = x ============================ ?x = 0 -1 focused subgoal +1 focused goal (shelved: 1) H : forall x : nat, S (S (S x)) = x ============================ ?x = 0 -1 focused subgoal +1 focused goal (shelved: 1) H : forall x : nat, S x = x diff --git a/test-suite/success/autorewrite.v b/test-suite/success/autorewrite.v index 71d333d439..0ac62fcdc9 100644 --- a/test-suite/success/autorewrite.v +++ b/test-suite/success/autorewrite.v @@ -4,25 +4,35 @@ Axiom Ack0 : forall m : nat, Ack 0 m = S m. Axiom Ack1 : forall n : nat, Ack (S n) 0 = Ack n 1. Axiom Ack2 : forall n m : nat, Ack (S n) (S m) = Ack n (Ack (S n) m). -Hint Rewrite Ack0 Ack1 Ack2 : base0. +Module M. + #[export] Hint Rewrite Ack0 Ack1 Ack2 : base0. -Lemma ResAck0 : (Ack 2 2 = 7 -> False) -> False. + Lemma ResAck0 : (Ack 2 2 = 7 -> False) -> False. + Proof. + intros. + autorewrite with base0 in H using try (apply H; reflexivity). + Qed. +End M. + +Lemma ResAck1 : forall H:(Ack 2 2 = 7 -> False), True -> False. Proof. intros. - autorewrite with base0 in H using try (apply H; reflexivity). -Qed. + Fail autorewrite with base0 in *. +Abort. + +Import M. Lemma ResAck1 : forall H:(Ack 2 2 = 7 -> False), True -> False. Proof. intros. autorewrite with base0 in *. - apply H;reflexivity. + apply H;reflexivity. Qed. (* Check autorewrite does not solve existing evars *) (* See discussion started by A. Chargueraud in Oct 2010 on coqdev *) -Hint Rewrite <- plus_n_O : base1. +Global Hint Rewrite <- plus_n_O : base1. Goal forall y, exists x, y+x = y. eexists. autorewrite with base1. Fail reflexivity. diff --git a/test-suite/success/forward.v b/test-suite/success/forward.v index 4e36dec15b..62c788e910 100644 --- a/test-suite/success/forward.v +++ b/test-suite/success/forward.v @@ -27,3 +27,7 @@ Fail match goal with |- (?f ?a) => idtac end. (* should be beta-iota reduced *) 2:match goal with _: (?f ?a) |- _ => idtac end. (* should not be beta-iota reduced *) Abort. +Goal nat. +assert nat as J%S by exact 0. +exact J. +Qed. diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index 4983ee3c0d..615350c58c 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -154,50 +154,6 @@ induction H. change (0 = z -> True) in IHrepr''. Abort. -(* Test double induction *) - -(* This was failing in 8.5 and before because of a bug in the order of - hypotheses *) - -Set Warnings "-deprecated". - -Inductive I2 : Type := - C2 : forall x:nat, x=x -> I2. -Goal forall a b:I2, a = b. -double induction a b. -Abort. - -(* This was leaving useless hypotheses in 8.5 and before because of - the same bug. This is a change of compatibility. *) - -Inductive I3 : Prop := - C3 : forall x:nat, x=x -> I3. -Goal forall a b:I3, a = b. -double induction a b. -Fail clear H. (* H should have been erased *) -Abort. - -(* This one had quantification in reverse order in 8.5 and before *) -(* This is a change of compatibility. *) - -Goal forall m n, le m n -> le n m -> n=m. -intros m n. double induction 1 2. -3:destruct 1. (* Should be "S m0 <= m0" *) -Abort. - -(* Idem *) - -Goal forall m n p q, le m n -> le p q -> n+p=m+q. -intros *. double induction 1 2. -3:clear H2. (* H2 should have been erased *) -Abort. - -(* This is unchanged *) - -Goal forall m n:nat, n=m. -double induction m n. -Abort. - (* Mentioned as part of bug #12944 *) Inductive test : Set := cons : forall (IHv : nat) (v : test), test. diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index d37ad9f528..b8fbff05c6 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -152,3 +152,15 @@ Definition d := ltac:(intro x; exact (x*x)). Definition d' : nat -> _ := ltac:(intros;exact 0). End Evar. + +Module Wildcard. + +(* We check that the wildcard internal name does not interfere with + user fresh names (currently the prefix is "_H") *) + +Goal nat -> bool -> nat -> bool. +intros _ ?_H ?_H. +exact _H. +Qed. + +End Wildcard. diff --git a/test-suite/success/let_pattern_mismatch.v b/test-suite/success/let_pattern_mismatch.v new file mode 100644 index 0000000000..a56a8fff4f --- /dev/null +++ b/test-suite/success/let_pattern_mismatch.v @@ -0,0 +1,18 @@ +(* Weird corner case accepted by the pattern-matching algorithm. Destructuring + let-bindings in patterns can actually be shorter than the case they match. *) + +Inductive ascii : Set := +| Ascii : bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> ascii. + +Definition dummy (a : ascii) : unit := + let (a0,a1,a2,a3,a4,a5,a6,a7) := a in tt. + +Goal forall (a : ascii) (H : tt = dummy a), True. +Proof. +intros a H. +unfold dummy in *. +(* Two bound variables in the pattern, eight in the term. *) +match goal with +| H:context [ let (x, y) := ?X in _ ] |- _ => destruct X eqn:? +end. +Abort. diff --git a/test-suite/success/match_case_pattern_variables.v b/test-suite/success/match_case_pattern_variables.v new file mode 100644 index 0000000000..bb9117d033 --- /dev/null +++ b/test-suite/success/match_case_pattern_variables.v @@ -0,0 +1,34 @@ +(** Check that bound variables in case patterns are handled correctly. *) + +Goal forall (ch : unit) (t : list unit) (s : list unit), + match s with + | nil => False + | cons a l => ch = a /\ l = t + end. +Proof. +intros. +match goal with +| |- match ?e with + | nil => ?N + | cons a b => ?P + end => + let f := + constr:((fun (e' : list unit) => match e' with + | nil => N + | cons a b => P + end)) + in + change (f e) +end. +Abort. + +Goal forall (ch : unit) (n : nat) (s : prod unit nat), + let (a, l) := s in ch = a /\ l = n. +Proof. +intros. +match goal with +| [ |- let (a, b) := ?e in ?P ] => + let f := constr:((fun (e' : prod unit nat) => match e' with pair a b => P end)) in + change (f e) +end. +Abort. |