test-suite/bugs/closed/bug_3228.v


1
2
3
4
5
6
7
8

(* Check that variables in the context do not take precedence over
   ltac variables *)

Ltac bar x := exact x.
Goal False -> False.
  intro x.
  Fail bar doesnotexist.
Abort.