summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/3957.v
blob: e20a6e97f09707300c96fc003db14551b1f15841 (plain)
1
2
3
4
5
6
Ltac foo tac := tac.

Goal True.
Proof.
foo subst.
Admitted.