diff options
| author | Enrico Tassi | 2019-01-17 16:17:41 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-01-18 19:05:36 +0100 |
| commit | 2f3db0b605b3aa345c1fea26c263ba6793a0fa51 (patch) | |
| tree | e2a10ec2f26d61149129b776693cb4af5cf259a6 /test-suite | |
| parent | f059d18c411b4c9e2abba6d158b3a125916f38dc (diff) | |
[ssr] compile "=> {} y" as "=> {y} y"
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. |