aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/2818.v
blob: 010855cfb77553a67bdbb58771aa7887177713b1 (plain)
1
2
3
4
5
6
7
8
9
10
11
Module M.

Local Ltac t := exact I.
Ltac u := t.

End M.

Goal True.
Proof.
M.u.
Qed.