diff options
| author | Enrico Tassi | 2019-01-17 18:01:42 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-01-19 17:19:43 +0100 |
| commit | 1b9c386bb5118145f0a2b46c523dd195d97c8413 (patch) | |
| tree | ad859989917a649369dbf2826b847792de2a8ce0 /test-suite | |
| parent | 762a47bce085bf1606a05c7b59c8a59803730eeb (diff) | |
[ssr] compile "=> {x..} y" as "=> {x..y} y"
This is for consistency with "rewrite {x..} y"
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/ssr/ipat_replace.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/ssr/ipat_replace.v b/test-suite/ssr/ipat_replace.v index 70e1d5bcf1..528f33f30d 100644 --- a/test-suite/ssr/ipat_replace.v +++ b/test-suite/ssr/ipat_replace.v @@ -9,9 +9,9 @@ have {}H : True. by apply: H. Qed. -Lemma test2 (H : True) : False -> False. +Lemma test2 (H : True) : False -> False -> False. Proof. -Fail move=> {}W. +move=> {}W. move=> {}H. by apply: H. Qed. |