Differential `'d f x` parsing rule gets shadowed by Radon-Nikodym derivative

[CohenCyril]

From mathcomp Require Import all_ssreflect all_algebra all_analysis.
Import GRing.Theory.
Open Scope ring_scope.

Check fun {R : realType} (f g : R -> R) => 'd f 0 = g.

errors

Error: Syntax error: ''/d' expected after [term] (in [term]).

[CohenCyril]

BTW the import warnings say:

Warning: Notations "'d _ _" defined at level 0 with arguments constr at level 0 and "'d _ '/d _"
defined at level 10 with arguments constr at next level have incompatible prefixes.
One of them will likely not work. [notation-incompatible-prefix,parsing,default]

[CohenCyril]

@proux01 do you know how to fix this?

[CohenCyril]

Apparently we also have the problem with other notations:

Warning: Notations "'o_ _" defined at level 200 with arguments constr at level 0 and "'o_ _ _" defined at level 0
with arguments constr at level 0 have incompatible prefixes. One of them will likely not work.
[notation-incompatible-prefix,parsing,default]
Warning: Notations "'o" defined at level 200 and "'o '_' _" defined at level 0 have incompatible prefixes.
One of them will likely not work. [notation-incompatible-prefix,parsing,default]
Warning: Notations "'o" defined at level 200 and "'o _( _ \near _ ) _" defined at level 0
have incompatible prefixes. One of them will likely not work. [notation-incompatible-prefix,parsing,default]
Warning: Notations "'O_ _" defined at level 200 with arguments constr at level 0 and "'O_ _ _" defined at level 0
with arguments constr at level 0 have incompatible prefixes. One of them will likely not work.
[notation-incompatible-prefix,parsing,default]
Warning: Notations "'O" defined at level 200 and "'O '_' _" defined at level 0 have incompatible prefixes.
One of them will likely not work. [notation-incompatible-prefix,parsing,default]
Warning: Notations "'O" defined at level 200 and "'O _( _ \near _ ) _" defined at level 0
have incompatible prefixes. One of them will likely not work. [notation-incompatible-prefix,parsing,default]
Warning: Notations "'M_ _" defined at level 0 with arguments constr at level 2 and "'M_ _ _" defined at level 5
with arguments constr at level 4 have incompatible prefixes. One of them will likely not work.
[notation-incompatible-prefix,parsing,default]
Warning: Notations "{ ' _ | _ }" defined at level 0 and "{ additive_charge set _ -> \bar _ }" defined at level 36
have incompatible prefixes. One of them will likely not work. [notation-incompatible-prefix,parsing,default]
Warning: Notations "{ ' _ | _ }" defined at level 0 and "{ charge set _ -> \bar _ }" defined at level 36
have incompatible prefixes. One of them will likely not work. [notation-incompatible-prefix,parsing,default]

[proux01]

Yes, as suggested by the warning, the Reserved Notation should be aligned (at least on the common prefix), here in derive.v and charge.v.
In fact, since charge.v requires derive.v, the simplest fix is to change the Reserved Notation there from

Reserved Notation "'d nu '/d mu" (at level 10, nu, mu at next level,
  format "''d'  nu  ''/d'  mu").

to

Reserved Notation "'d nu '/d mu" (mu at next level, format "''d'  nu  ''/d'  mu").

and it will automatically retrieves the other levels from derive.v.