diff options
| author | Enrico Tassi | 2020-02-28 16:51:24 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2020-02-28 16:51:24 +0100 |
| commit | 5c7d89641085e125471db089239e73a064073024 (patch) | |
| tree | d1a170a097b1b4b57232613948b3b7fec9f5865f /test-suite/bugs | |
| parent | aeca986089d005054496ed4bcf1b920e8fa02173 (diff) | |
| parent | 721b6704a0fbee1be627c67e0a883fa40a81deb6 (diff) | |
Merge PR #11609: [stm] Use Default Proof Using only with Proof
Diffstat (limited to 'test-suite/bugs')
| -rw-r--r-- | test-suite/bugs/closed/bug_11342.v | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_11342.v b/test-suite/bugs/closed/bug_11342.v new file mode 100644 index 0000000000..3c163fb772 --- /dev/null +++ b/test-suite/bugs/closed/bug_11342.v @@ -0,0 +1,19 @@ +(* -*- mode: coq; coq-prog-args: ("-vos") -*- *) + +Section foo. + Context {H:True}. + Set Default Proof Using "Type". + Theorem test2 : True. + Proof. + (* BUG: this gets run when compiling with -vos *) + fail "proof with default using". + exact I. + Qed. + + Theorem test3 : True. + Proof using Type. + (* this isn't run with -vos *) + fail "using". + exact I. + Qed. +End foo. |