During section closing, I'm looking to properly discharge the variables of the section in the data I keep. In particular, I want to discharge entire proof states (local context + conclusion). This is somewhat different from discharging constants, because no variable abstraction needs to occur. Only the correct variables need to be applied to constants that rely on them.
In Coq <= 8.15 I could use Cooking.expmod_constr for this purpose. It does exactly what I need: Apply the appropriate variables to every constant in a term. Since PR #14727 by @Hugo Herbelin, for Coq 8.16, this function has been completely removed though, and the cooking mechanism has been completely reworked. In the new API, I don't see any way to accomplish what I need, especially since all the cooking data is now kept pretty privately within the
Can anyone suggest a way to recover the functionality that was available through
Cooking.expmod_constr in Coq >= 8.16?
so you want expand_subst to be exposed?
I'm not entirely sure, but I don't think that will work. As far as I can see,
expand_subst does two things at once: (1) it applies the section variables to constants and (2) it immediately abstracts those section variables into de Bruijn indices. (Then the functions like
abstract_as_body add the actual lambda abstractions to the beginning of the term.) I need a function that only performs action (1).
Last updated: Nov 29 2023 at 05:01 UTC