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: Apr 19 2024 at 11:02 UTC