Emilio Jesús Gallego Arias

> Does it still sound like nonsense? You seem to focus on some criteria about refs vs parameter for things that change vs not. That's not the point of this...

@andres-erbsen thanks for the reference. Indeed I do remain puzzled because the methodology we are using (isolation of state) is pretty standard in large systems. Actually the origin of us...

Thanks for the bug report @jp-diegidio , a few comments: - the current behavior is selectable, controlled by the `coq-lsp.updateIgnores` setting - based on feedback from early users, we made...

I cannot reproduce in vscode 1.90 , is that still a problem for you @Alizter ? I think this may have been fixed by #755 and related PRs.

> What is the status of OCaml 5 support for Coq? Mixed, it works better for some users, worse for others. > Is it worth switching over as a default...

> What happens to the opam package? Do you just switch the source? `coq-lsp` wont' depend anymore on `coq-serapi` Newer `coq-serapi` will depend on `coq-lsp`, if there is a new...

This is because `Pff.v` entries in the memo table are still cached, but indeed it is not clear what to do. GC will do nothing in this case; you wanna...

Thanks Ali, I will tweak the working to say "serialize and display in a new window", as the command now opens a new windows.

It seems to me that program slicing as done in minimization do belong as a separate tool from coq-lsp/Flèche. But indeed, coq-lsp / Flèche can provide much better support for...

`.lv` files are mainly helpful for two reasons: - they help avoid inlining, which is often brittle and hard to implement. - the provide an _atomic_ and _incremental_ protocol for...