Stream: Coq devs & plugin devs

Topic: From opaque back to constr

view this post on Zulip 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?

Last updated: Nov 29 2023 at 21:01 UTC