You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
From mathcomp RequireImport all_ssreflect all_algebra all_analysis.
Reports
Notation "_ ``_ _" is already defined at level 3 with arguments constr at level 3, constr
at level 2 while it is now required to be at level 3 with arguments constr at next level, constr
at level 2.
Because forms.v (from analysis) and sesquilinear.v (from mathcomp) now have two incompatible reserve notion, the former has:
Reserved Notation "u '``_' i"
(at level 3, i at level 2, format "u '``_' i").
while the later has
Reserved Notation "u '``_' i"
(at level 3, i at level 2, left associativity, format "u '``_' i").
The text was updated successfully, but these errors were encountered:
Reports
Because
forms.v
(from analysis) andsesquilinear.v
(from mathcomp) now have two incompatible reserve notion, the former has:while the later has
The text was updated successfully, but these errors were encountered: