vscoq incorrectly parses `(@` as not a valid in constr scope when ssreflect is (transitively) `Require`d

[JasonGross]

Proof using Type. is perfectly valid, but somehow vscoqtop does not see this. Presumably it has somehow gotten desynchronized from the document state?

[JasonGross]

Apparently it's complaining because it thinks (@ is not valid, but make builds this file fine on the commandline

[JasonGross]

Can anyone else confirm whether or not this is an issue on my machine or if vscoq is incapable of handling https://github.com/mit-plv/fiat-crypto/blob/847d6a74e7205e8010ff9e2f405f6d30f100978a/src/Assembly/WithBedrock/SymbolicProofs.v#L351 ?

[JasonGross]

Seems like it's a problem handling (@ in Ltac?

[JasonGross]

I am also getting this with

Derive rewrite_pass_Listable SuchThat (@FinitelyListable rewrite_pass rewrite_pass_Listable) As rewrite_pass_FinitelyListable.
Proof. prove_ListableDerive. Qed.
Global Existing Instances rewrite_pass_Listable rewrite_pass_FinitelyListable.

[gares]

I think I've seen a problem with some Ltac notations before, but I never managed to pin it down. Thanks for reporting this issue.

[JasonGross]

Is this slated to be fixed soon? It's quite frustrating to have vscoq be unable to handle files with (@, since this is pretty common

[JasonGross]

Is there any way to invoke the thing that vscoq does on reloading the window from the command line? Currently I've narrowed down the issue to

Require Import Crypto.Assembly.Symbolic.
Definition foo := Set.
Check (@foo).

[JasonGross]

Okay, here's a minimal-ish reproducing example:

From Coq Require Import ssreflect.
Definition foo := Set.
Check (@foo).

[JasonGross]

More minimized:

Declare ML Module "rocq-runtime.plugins.ssreflect".
Definition foo := Set.
Check (@foo).

[gares]

Thanks!