summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/shouldfail/1703.v
blob: 6b5198cc03c9414366b5fbc6ef46ffee21495e4e (plain)
1
2
3
4
5
6
7
(* Check correct binding of intros until used in Ltac *)

Ltac intros_until n := intros until n.

Goal forall i j m n : nat, i = 0 /\ j = 0 /\ m = 0 /\ n = 0.
intro i.
intros until i.