Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

stdlib exports conflicting notations #4

Open
andres-erbsen opened this issue Dec 20, 2024 · 0 comments
Open

stdlib exports conflicting notations #4

andres-erbsen opened this issue Dec 20, 2024 · 0 comments

Comments

@andres-erbsen
Copy link
Contributor

andres-erbsen commented Dec 20, 2024

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)

Originally posted by @SkySkimmer in coq/coq#19914 (comment)

@proux01 proux01 transferred this issue from coq/coq Jan 13, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant