varkor

> We currently have no appeals to eauto, so portability would be enhanced by not admitting its use. Is there anywhere the reasoning behind the portability arguments is set forth?...

No-one is suggesting we change the name. Using an enum instead of a bool would simplify some special-casing in the compiler, which would be an advantage.

@jhpratt: there was a [brief discussion on](https://discordapp.com/channels/442252698964721669/443151243398086667/570238506018799626) Discord about it a while ago. You'd probably want to talk to @oli-obk or @eddyb about it if you wanted to pursue it,...

We can keep the keywords and have them refer to the variants of the enum. There might be some diagnostics changes to work out, but I don't think it'd be...

I'm not sure if this is the same issue, but sometimes only closing the window and reopening it will fix a Coq error — even `Coq: Reset` does not suffice.

@dbshch: there's a `> Coq: Reset` command does this.

There seem to be two problems here. One is that there are a number of TypeScript errors. The second is that `vsce` has trouble accessing the file `vscoq/client/.testUser/user/1.20.1-main.sock`. I'm not...

I'm not sure if this is directly related, but VS Code's new "Dynamic Previews" for Markdown look very useful for VSCoq (instead of opening lots of new proof views): https://code.visualstudio.com/updates/v1_21#_markdown-dynamic-previews

@chantisnake: it does seem unlikely that this branch will be updated in the near future. I might consider forking the plugin, though I don't have time right now: I'd want...

This is a duplicate of https://github.com/siegebell/vscoq/issues/143. It's really annoying, but it's actually a longstanding bug with Electron (see https://github.com/Microsoft/vscode/issues/44070 and https://github.com/electron/electron/issues/2617). I think one of the workarounds worked for me,...