Jason Gross

It looks like a real issue, but unrelated to this PR. Should be fixed by https://github.com/mit-plv/fiat-crypto/pull/1842, if the error message is accurate.

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

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 ?

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

I am also getting this with ```coq 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. ```

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

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 ```coq Require Import Crypto.Assembly.Symbolic....

Okay, here's a minimal-ish reproducing example: ```coq From Coq Require Import ssreflect. Definition foo := Set. Check (@foo). ```

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

@coqbot CI minimize ci-metacoq