I have two external modules(the sources of which are better not to be alternated) which define the same notation. The consequence of this is I am now not able to import both module at the same time anymore, due to this error:
Error: Notation _ ~ _ is already defined at level 27 with arguments at level 27,
at next level while it is now required to be at level 50 with arguments at next level,
at next level.
Is there any way out? I would imagine either not importing notations from one module, or only do selective importation. However, looking through the documentation does not say too much about it.
any chance I looked over? or what solution will you recommend?
The short answer is unfortunately no. Upstream is aware of this limitation and at some point in the future (Coq 8.9?) you will hopefully able to do this using "parsing tables".
However, there is an acceptable workaround: use sections to limit the scope of your import. Imagine modules a b define a conflicting notation, then you can do:
Require a b.
Section WithNotationA.
Import a.
...
End WithNotationA.
Section WithNotationB.
Import b.
...
End WithNotationB.