We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
8.8.2
Arch Linux, up to date within one week.
Goal True. assert_succeeds (exact I). idtac. (* Error: No such goal. *) Abort.
The text was updated successfully, but these errors were encountered:
assert_fails too.
assert_fails
Sorry, something went wrong.
I think this definition might solve both issues?
Ltac assert_fails tac := tryif (cut True; [ intros _; tac | ]) then fail 0 tac "succeeds" else idtac.
Fix coq#9114, assert_succeeds (exact I) solves goal
53a9487
assert_succeeds
Use a less kludgy way of solving coq#9114
b213691
c9adfcd
Successfully merging a pull request may close this issue.
Version
8.8.2
Operating system
Arch Linux, up to date within one week.
Description of the problem
The text was updated successfully, but these errors were encountered: