summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/1703.v
blob: 114e3185b835db89cb8fe3ef5458bc6376267b7e (plain)
1
2
3
4
5
6
7
8
(* 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.
Fail intros until i.
Abort.