aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4221.v
blob: bc120fb1ff991526148d55d69a5cbdf64d747702 (plain)
1
2
3
4
5
6
7
8
9
(* 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.