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?
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 := ...).
For scopes declaration, I'm not sure, but if a prefixed
Global does not work, nothing does afaik.
FWIW: almost everything works in a module, since everything is defined in a module.
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: Jan 31 2023 at 14:03 UTC