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 `Overrider`

last.

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:

https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq:cmd.Require-Import

https://coq.inria.fr/refman/language/core/modules.html#coq:cmd.Import

https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#coq:cmd.Notation

are you using Export somewhere?

probably yes — there are ~307 occurrences of `Export`

in this codebase

uuuh, there is a chain of `Export`

s 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