aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/ErrorLocation_ltac_4.v
AgeCommit message (Expand)Author
2020-09-16More improvements in locating tactic errors.Hugo Herbelin