-
Notifications
You must be signed in to change notification settings - Fork 643
New issue
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
Handle delayed opaque proofs in Print Assumptions #14382
Conversation
bc0c623
to
382c226
Compare
https://gitlab.com/coq/coq/-/jobs/1291081315 is not happy |
@SkySkimmer yes, it seems like the binary called by the script doesn't like the |
Instead of using Global.body_of_constant_body and tinkering with the result we roll up our own version of the accessor which is delayed-proof-aware. Fixes coq#13589: Print Assumptions for vok.
I find the code clearer that way, as it clearly indicates intent.
382c226
to
060deaf
Compare
Let's try a bit of cargo culting to see whether it works. I mimicked the script in the vos folder, which calls the |
I guess -vok is passed to the worker (incorrectly). |
060deaf
to
198acb4
Compare
Seems to be OK now. |
@coqbot: merge now |
Instead of using Global.body_of_constant_body and tinkering with the result we roll up our own version of the accessor which is delayed-proof-aware.
Fixes #13589: Print Assumptions for vok.
Supersedes #13614.