aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/ErrorLocation_12255.v
AgeCommit message (Collapse)Author
2020-05-25Fix output tests for location errors when running in async mode.Théo Zimmermann
In this mode, an additional error was emitted, which made the test fail: Error: There are pending proofs: Unnamed_thm.
2020-05-10Adding tests for error locationHugo Herbelin