aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/ErrorLocation_ltac_1.out
blob: a9014c4b4696cdefba0cb2b57689109cca29bd9c (plain)
1
2
3
File "stdin", line 2, characters 7-11:
Error: Tactic failure: Cannot solve this goal.