diff options
| author | Pierre-Marie Pédrot | 2020-08-26 00:43:45 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-26 00:43:45 +0200 |
| commit | e01f9df8aa68ecae26bce15544b7244ced1b2be5 (patch) | |
| tree | 2076e0c62e8e571dc64d2775377f6dd24ffabea9 /test-suite | |
| parent | 51c0d56a5b0384e2f6bd980a1111547641c66b3e (diff) | |
| parent | 4ad36b5e2369b37aa2483a1e04eb628d147d97d3 (diff) | |
Merge PR #12861: Require NsatzTactic: nsatz support for Z and Q
Ack-by: Zimmi48
Reviewed-by: jfehrle
Reviewed-by: ppedrot
Reviewed-by: thery
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_12860.v | 10 |
1 files changed, 10 insertions, 0 deletions
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. |