aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/ErrorLocation_ltac_2.out
blob: d38727ffa495d1ebdce1adccdf8ea904df7f200a (plain)
1
2
3
File "stdin", line 3, characters 7-8:
Error: Tactic failure.