Localized notation #
This consists of two user-commands which allow you to declare notation and commands localized to a locale.
See the tactic doc entry below for more information.
The code is inspired by code from Gabriel Ebner from the hott3 repository.
Execute all commands in the given locale
Add a new command to a locale and execute it right now.
The new command is added as a declaration to the environment with name _localized_decl.<number>
.
This declaration has attribute _localized
and as value a name-string pair.