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
File "./theories/All.v", line 3, characters 0-12361:
Warning: Notations "_ ^^ _" defined at level 30 with arguments constr
at next level, constr at level 30 and "_ ^^ _ --> _" defined at level 50
with arguments constr at next level, constr at next level
have incompatible prefixes. One of them will likely not work.
[notation-incompatible-prefix,parsing,default]
Zpower_alt infix vs some deprecated notation in NaryFunctions
File "./theories/All.v", line 3, characters 0-12361:
Warning: Notation "[ _ ]" was already used.
[notation-overridden,parsing,default]
rtauto vs vector
File "./theories/All.v", line 3, characters 0-12361:
Warning: Notation "[ _ ]" was already used.
[notation-overridden,parsing,default]
nsatz vs rtauto
File "./theories/All.v", line 3, characters 0-12361:
Warning: Overwriting previous delimiting key B in scope bool_scope
[overwriting-delimiting-key,parsing,default]
ssrbool vs datatypes
File "./theories/All.v", line 3, characters 0-12361:
Warning: Notation "_ === _" was already used in scope equiv_scope.
[notation-overridden,parsing,default]
File "./theories/All.v", line 3, characters 0-12361:
Warning: Notation "_ =/= _" was already used in scope equiv_scope.
[notation-overridden,parsing,default]
File "./theories/All.v", line 3, characters 0-12361:
Warning: Notation "_ =~= _" was already used in scope equiv_scope.
[notation-overridden,parsing,default]
CEquivalence vs Equivalence
File "./theories/All.v", line 3, characters 0-12361:
Warning: Notation "_ == _" was already used.
[notation-overridden,parsing,default]
setoid_ring.Algebra_syntax vs setoids
File "./theories/All.v", line 3, characters 0-12361:
Warning: Notation "_ ==b _" was already used.
[notation-overridden,parsing,default]
File "./theories/All.v", line 3, characters 0-12361:
Warning: Notation "_ <>b _" was already used.
[notation-overridden,parsing,default]
EquivDec vs SetoidDec (these 2 files are pretty similar, not sure why we have both)
Zpower_alt infix vs some deprecated notation in NaryFunctions
rtauto vs vector
nsatz vs rtauto
ssrbool vs datatypes
CEquivalence vs Equivalence
setoid_ring.Algebra_syntax vs setoids
EquivDec vs SetoidDec (these 2 files are pretty similar, not sure why we have both)
Originally posted by @SkySkimmer in coq/coq#19914 (comment)
The text was updated successfully, but these errors were encountered: