diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/ssr/autoclean.v | 4 | ||||
| -rw-r--r-- | test-suite/stm/arg_filter_1.v | 4 |
2 files changed, 6 insertions, 2 deletions
diff --git a/test-suite/ssr/autoclean.v b/test-suite/ssr/autoclean.v new file mode 100644 index 0000000000..db80a62259 --- /dev/null +++ b/test-suite/ssr/autoclean.v @@ -0,0 +1,4 @@ +Require Import ssreflect. + +Lemma view_disappears A B (AB : A -> B) : A -> False. +Proof. move=> {}/(AB). have := AB. Abort. diff --git a/test-suite/stm/arg_filter_1.v b/test-suite/stm/arg_filter_1.v index 1cf66d6b43..ed87d67405 100644 --- a/test-suite/stm/arg_filter_1.v +++ b/test-suite/stm/arg_filter_1.v @@ -1,4 +1,4 @@ (* coq-prog-args: ("-async-proofs-tac-j" "1") *) -Lemma foo : True. -Proof. now auto. Qed. +Lemma foo (A B : Prop) n : n + 0 = n /\ (A -> B -> A). +Proof. split. par: now auto. Qed. |