I'm trying to use both Setoid rewrite and math-comp classical. But importing both is impossible due to a conflict in the notation declaration:
From Corelib Require Import Setoid.
From mathcomp Require Import filter.
raise the error
Error: Notation "_ --> _" is already defined at level 55 with arguments constr
at next level, constr at level 55 while it is now required to be at level 70
with arguments constr at next level, constr at next level.
I'm trying to use both Setoid rewrite and math-comp classical. But importing both is impossible due to a conflict in the notation declaration:
raise the error