Stream: Coq devs & plugin devs

Topic: Does `Register` persist outside of a section?


view this post on Zulip Ali Caglayan (Nov 24 2022 at 18:18):

If I put Register in a section, will it continue when the section is closed?

view this post on Zulip Ali Caglayan (Nov 24 2022 at 18:59):

Looks like yes


Last updated: Feb 06 2023 at 19:03 UTC