[notation-overridden,parsing,default] on all_ssreflect import

[0xGeorgii]

Hi. I just installed vscoq extension alongside the LS and ssreflect and on the import I see the following errors:

From mathcomp Require Import all_ssreflect.

Can you please help solve this problem? I use Ubuntu23.10

[0xGeorgii]

Fixed by reducing to

From mathcomp Require Import ssreflect seq.

but what interfered?

[SkySkimmer]

These are warnings not errors.

[0xGeorgii]

These are warnings not errors.

but I suppose they should not be

[TheoWinterhalter]

They're warnings of Coq, not of VSCoq. I agree that this is annoying, but this should be a bug for mathcomp I think.

[rtetley]

Pinging @gares