Stream: Coq devs & plugin devs

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

Ali Caglayan (Nov 24 2022 at 18:18):

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

Ali Caglayan (Nov 24 2022 at 18:59):

Looks like yes

Last updated: Dec 06 2023 at 14:01 UTC