diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_12676.v | 13 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_12860.v | 10 | ||||
| -rw-r--r-- | test-suite/output/ssr_error_multiple_intro_after_case.v | 1 |
3 files changed, 24 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_12676.v b/test-suite/bugs/closed/bug_12676.v new file mode 100644 index 0000000000..5118ddb472 --- /dev/null +++ b/test-suite/bugs/closed/bug_12676.v @@ -0,0 +1,13 @@ + + +Definition nat_eq_dec(i j:nat) : {i=j}+{i<>j}. +Proof. + pose (diseq := false). + decide equality. +Defined. + +Set Mangle Names. +Definition nat_eq_dec_mangle (i j:nat) : {i=j}+{i<>j}. +Proof. + decide equality. (*Error: Anomaly "variable diseq unbound." ...*) +Defined. diff --git a/test-suite/bugs/closed/bug_12860.v b/test-suite/bugs/closed/bug_12860.v new file mode 100644 index 0000000000..243aeceba2 --- /dev/null +++ b/test-suite/bugs/closed/bug_12860.v @@ -0,0 +1,10 @@ +Require Import Coq.nsatz.NsatzTactic. +Require Import Coq.ZArith.ZArith Coq.QArith.QArith. + +Goal forall x y : Z, (x + y = y + x)%Z. + intros; nsatz. +Qed. + +Goal forall x y : Q, Qeq (x + y) (y + x). + intros; nsatz. +Qed. diff --git a/test-suite/output/ssr_error_multiple_intro_after_case.v b/test-suite/output/ssr_error_multiple_intro_after_case.v index 1f87966693..18997b8686 100644 --- a/test-suite/output/ssr_error_multiple_intro_after_case.v +++ b/test-suite/output/ssr_error_multiple_intro_after_case.v @@ -1,3 +1,4 @@ Require Import ssreflect. Goal forall p : nat * nat , True. case => x x. +Abort. |