search

coq-community / vscoq

A Visual Studio Code extension for Coq [maintainers=@rtetley,@huynhtrankhanh,@thery,@Blaisorblade]
MIT License
328 stars 68 forks source link

[notation-overridden,parsing,default] on `all_ssreflect` import #692

Open 0xGeorgii opened 9 months ago

0xGeorgii commented 9 months ago

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.

image

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

0xGeorgii commented 9 months ago

Fixed by reducing to

From mathcomp Require Import ssreflect seq.

but what interfered?

SkySkimmer commented 9 months ago

These are warnings not errors.

0xGeorgii commented 9 months ago

These are warnings not errors.

but I suppose they should not be

TheoWinterhalter commented 9 months ago

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 commented 9 months ago

Pinging @gares