diff options
| author | Maxime Dénès | 2019-01-28 13:32:36 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-01-28 13:32:36 +0100 |
| commit | 562a731fd380be3e3ba8318348a9b92ca6cc1668 (patch) | |
| tree | 55cede7a7756e02178e012af27e9801cca0a3567 /test-suite | |
| parent | 5aa4b87d4ed71a22a696ae73af77ced8f5c6da47 (diff) | |
| parent | 932880e247e963116b576701e76ce18b3450bec1 (diff) | |
Merge PR #9341: [ssr] uniform clear discipline
Reviewed-by: CohenCyril
Ack-by: Zimmi48
Ack-by: gares
Reviewed-by: maximedenes
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..528f33f30d --- /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 -> False. +Proof. +move=> {}W. +move=> {}H. +by apply: H. +Qed. |