Jason Gross (Oct 30 2023 at 20:03): Jason Gross (Oct 30 2023 at 20:03):What's the plan for global mutable state in Ltac2 (a la https://github.com/coq/coq/pull/13982, cf https://github.com/coq/coq/issues/18109#issuecomment-1743268647)? Even the version that only persists until a . would be useful for a convenience fresh tactic that does not give duplicate names and hence doesn't require maintaining the map of used identifiers by hand. Having effects that persist past . would also be nice (e.g., caching on the side, etc) but I'd like to see at least the ability to avoid passing around a global state object to every tactic that wants to have not-recordable-in-proof-state side effects.
Pierre-Marie Pédrot (Oct 30 2023 at 23:04):Global tables are on the roadmap, I definitely have to work on this soon.
Last updated: Oct 12 2024 at 12:01 UTC