I have a file with a section with a few
Hint Constructors : core. I'm
Require Importing this file in another one, but my notations and hints doesn't seem available. Do I have to do something in the first file to make notations and hitns available outside of the file/section ?
I'm scanning the doc but only find things about notation scopes (like
This command supports the local attribute, which limits its effect to the current module. If the command is inside a section, its effect is limited to the section.
It's because notations and tactics do not have a straightforward generalisation. The only solution is to define them again after closing the section.
Will do. Thanks !
Vincent Siles has marked this topic as resolved.
Last updated: Jan 31 2023 at 12:01 UTC