Lasse Blaauwbroek (Sep 12 2022 at 11:57): Lasse Blaauwbroek (Sep 12 2022 at 11:57):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 Cooking and Section modules.
Can anyone suggest a way to recover the functionality that was available through Cooking.expmod_constr in Coq >= 8.16?
Gaëtan Gilbert (Sep 12 2022 at 12:08):so you want expand_subst to be exposed?
Lasse Blaauwbroek (Sep 12 2022 at 12:12):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: Sep 09 2024 at 05:02 UTC