Stream: Coq devs & plugin devs

Topic: Fail catches anomaly and errors the same way


view this post on Zulip Matthieu Sozeau (Jun 12 2020 at 12:42):

I'd like to have a variant of Fail called Fail_no_anomaly (or similar) that succeeds only when the command raises a regular error and not an anomaly for writing test-suite files, we don't have anything simillar yet, right?

view this post on Zulip Gaëtan Gilbert (Jun 12 2020 at 13:18):

I thought Fail doesn't catch anomalies?

view this post on Zulip Théo Zimmermann (Jun 12 2020 at 13:22):

It doesn't indeed (at least it has been that way from 8.5 to 8.11).

view this post on Zulip Matthieu Sozeau (Jun 12 2020 at 13:25):

Ok, so that's my bad I must be catching one in Equations, thanks!


Last updated: Oct 21 2021 at 22:02 UTC