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.
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...
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