summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/4316.v
blob: 68dec1334a9f8f79b951bacdb74241d94c967f93 (plain)
1
2
3
Ltac tac := idtac.
Reset tac.
Ltac tac := idtac.