Problem with use of ssrfun

[rjraya]

I get:

Error: Notation "_ .[ _ ]" is already defined at level 2
with arguments constr at level 2, constr at level 200
while it is now required to be at level 2 with arguments constr
at level 2, constr Unknown level.

while compiling line:

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.

from ./AutosubstSsr.v

I temporarily solved it by explicitly naming ssrfun.omap but this makes me rename the rest of the examples.

I'm using Coq 8.11.1

[RalfJung]

Interesting; this still works fine with Coq 8.10 but broke with Coq 8.11. Not sure if thare is much we can do about it, notations are inherently non-modular...