diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/ssr/ipat_replace.v | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/test-suite/ssr/ipat_replace.v b/test-suite/ssr/ipat_replace.v new file mode 100644 index 0000000000..70e1d5bcf1 --- /dev/null +++ b/test-suite/ssr/ipat_replace.v @@ -0,0 +1,17 @@ +Require Import ssreflect. + +Lemma test : True. +Proof. +have H : True. + by []. +have {}H : True. + by apply: H. +by apply: H. +Qed. + +Lemma test2 (H : True) : False -> False. +Proof. +Fail move=> {}W. +move=> {}H. +by apply: H. +Qed. |