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!
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: Feb 05 2023 at 14:02 UTC