math-comp / math-comp

Mathematical Components
https://math-comp.github.io
573 stars 112 forks source link

`Import fingroup ssralg` broken #1257

Open Tragicus opened 1 month ago

Tragicus commented 1 month ago

On master, when I do From mathcomp Require Import fingroup ssralg I get the error Level 2 is already declared to have right associativity while it is now expected to have left associativity. This does not happen if I swap them.

gares commented 1 month ago

This must be a notation without an explicit associativity. Coq is "smart", if a notation has no assoc but collides with an existing one, then it re-uses the declared assoc; if a notation has no assoc and no colliding notation, then it picks one and then complains if the same notation is later declared with a different assoc (different from the one Coq picked).

Tragicus commented 1 month ago

I see, adding left associativity in fingroup.v somewhere solved it. I check that everything still compiles and if so I push.