blob: 54c75e344c342313c9588851e6d47bd1cf2084c1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
Goal False.
intuition
match goal with
| |- _ => idtac " foo"
end.
lazymatch goal with _ => idtac end.
match goal with _ => idtac end.
unshelve lazymatch goal with _ => idtac end.
unshelve match goal with _ => idtac end.
unshelve (let x := I in idtac).
Abort.
Require Import ssreflect.
Goal True.
match goal with _ => idtac end => //.
Qed.
|
