EDIT: this problem might require more circumstances to trigger.
I'd like to override an existing notation for an existing scope, but I'm not sure that's possible
and this might have gotten worse in 8.11.
AFAICT, it's not enough to do
(* Overrider module *) Require Import notation_source. (* Override notation *)
because clients of
Overrider might still get the original notation, unless they import
Are the side effects of the original module re-executed at every transitive import? That might make sense if somebody imports
notation_source directly, but I see
notation_source winning even in source files that never mention it.
I'm not sure I see relevant docs here:
are you using Export somewhere?
probably yes — there are ~307 occurrences of
Export in this codebase
uuuh, there is a chain of
Exports leading to
notation_source, which could explain this on its own :-|.
I guess that's what you meant @Gaëtan Gilbert ? Thanks a lot!
I'll look into it
yup, there is no transitive import without export
and crucially, no superglobal effects are involved
Last updated: Oct 05 2023 at 02:01 UTC