Enzo Crance (Dec 09 2021 at 15:37): Enzo Crance (Dec 09 2021 at 15:37):Hello. I've been told my elpi tactic would reintroduce a previously reverted section variable into the context, as if the revert tactic had not been called before. In your opinion, might this weird behaviour be due to Coq-Elpi, or is revert just broken when used on section variables? Thanks!
Enrico Tassi (Dec 09 2021 at 16:18):section variables should not be reverted (nor cleared), it is a can of worms.
elpi sees them as global constants.
maybe things go south if you clean them...
Last updated: Oct 13 2024 at 01:02 UTC