Philipp G. Haselwarter (Dec 03 2020 at 17:00): Philipp G. Haselwarter (Dec 03 2020 at 17:00):When Ltac definitions and Scope declarations are made inside (1) a section or (2) a module, is that definition / scope accessible in some way after the section/module is closed?
Fabian Kunze (Dec 03 2020 at 19:04):For a section, there is no hope for ltac-definitions to be visible outside (how would one generalize an tactic that is exact n for a section variable n after closing the section?). from a Module M, a tactic t defined in it is simply available as M.t (assuming you used Ltac t := ...).
Fabian Kunze (Dec 03 2020 at 19:07):For scopes declaration, I'm not sure, but if a prefixedGlobal does not work, nothing does afaik.
Paolo Giarrusso (Dec 03 2020 at 23:05):FWIW: almost everything works in a module, since everything is defined in a module.
Paolo Giarrusso (Dec 03 2020 at 23:08):the main (huge) exception is that "nested" modules are always Required with their containing module, so side effects that act on Require can only be disabled on top-level modules (by not requiring them, not even transitively), but not on "nested" modules (since you always get them when you require the containing module).
Last updated: Sep 23 2023 at 15:01 UTC