Stream: Elpi users & devs

Topic: Revert on section variable "forgotten" by an elpi tactic

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

view this post on Zulip 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: Jun 06 2023 at 21:01 UTC