Paolo G. Giarrusso

I believe this is ready. There was one point of contention, but I prefer to follow the user options accurately (as we always do) over trying to second-guess them in...

@andreiburdusa Your example is printed as a notation*, so the `Implicit` setting will not have an effect; you must first disable notations via `Coq: Display Notations`, and _then_ the `Implicit`...

Upstream issue: https://github.com/coq/coq/issues/16080. And https://github.com/coq/coq/issues/5178 is a different but related one.

Ah, this is a bug in either `node_modules/string-argv/index.js` or the code below in `server/src/CoqProject.ts` — neither strips comment lines at all, they just skip words. ```typescript private static parseCoqProject(text: string)...

I've now noticed that Proof General does not implement the desired behavior either, but hopefully we can still refuse compatibility with PG... If I add `# -arg -noinit` in `_CoqProject`,...

I've learned a (relevant?) alternative from @gstew5: the "Dev Containers" extension can deal with VsCoq by installing it _inside_ the container: https://marketplace.visualstudio.com/items?itemName=ms-vscode-remote.remote-containers (I'm on M1 and run into https://github.com/microsoft/vscode-remote-release/issues/8169, but...

I'm testing this locally, and it seems indeed useful enough to merge — if we were worried about regressions, we could probably add another option flag, but for now I...

Closed. Sorry for the slow reaction — this was a good change.

This is still a problem, and @thery might have asked about this in https://github.com/coq-community/vscoq/pull/327: > Another question, when I have several ProofView, I'd like that the one that receives a...

Wait I must be missing something: shouldn't the existing patch be included in 0.3.6 from last January? And indeed, MR #223 is where `Could not detect coqtop version, defaulting to...