blob: 6798c1ae4d3ed5862dbb626b46cb9cd34b9fd96d (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
(* Test surgical use of beta-iota in the type of variables coming from
pattern-matching for refine *)
Goal forall x : sigT (fun x => x = 1), True.
intro x; refine match x with
| existT _ x' e' => _
end.
lazymatch goal with
| [ H : _ = _ |- _ ] => idtac
end.
Abort.
|
