blob: f433c854555ec3206139fc4ba62b853f5daa297e (
plain)
1
2
3
4
5
6
7
8
9
10
|
(* Some test checking that interpreting binder names using ltac
context does not accidentally break the bindings *)
Goal (forall x : nat, x = 1 -> False) -> 1 = 1 -> False.
intros H0 x.
lazymatch goal with
| [ x : forall k : nat, _ |- _ ]
=> specialize (fun H0 => x 1 H0)
end.
Abort.
|
