The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi,

> The current behavior is more or less to select the most recent notation.
> In particular, if there is a notation in the current file, it will take
> precedence over notations defined in other files. It seems about as
> intuitive to me as what you suggest.

I think that may explain a lot of the trouble we have been having with
notation.  It frequently happens that printing notations just fails
(i.e., it will not use the notation we want it to use for printing), and
then we will typically randomly reorder the imports at the top of the
file until it works again.  Depending on the order of imports
(transitively!) like this is very frustrating, and also very hard to debug.

I guess at some point we have to try and come up with a reduced example...

Kind regards,
Ralf