Arpan Agrawal (Jul 17 2023 at 18:55): Arpan Agrawal (Jul 17 2023 at 18:55):In Coq 8.9, the way to do this was:
Opaqueproof.force_proof (Global.opaque_tables ()) opaq
(where opaq is the opaque term)
I see that force_proof has been moved to the Global module, but I'm not sure if it does the same thing (it also takes a accessor argument that the force_proof in Opaqueproof did not). Is there another way to go from opaque terms to constr or do I modify my API to take the accessor argument as input from the user?
Thanks!
Last updated: Nov 29 2023 at 21:01 UTC