Emilio Jesús Gallego Arias

Update: coq-lsp supports this just by sending updated versions of a .v file to it; it will figure out what not to recompute by itself.

Yes, for now have not yet implemented any cache-eviction policy, we have researched actually quite a bit on what such strategies would be best, but so far sharing in practice...

For example a goal we have and we are actually close to achieve is going from: ```coq Lemma foo : T. Proof. by succesful_proof. Qed. Lemma bar: T. Proof. by...

Indeed, actually related to the discussion at https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs.20.26.20plugin.20devs/topic/Abort.20for.20modules.2Fprogram.3F , I do have something that could help. Even if you get access to the Coq's AST, it is still mostly a...

That's the correct thing to do indeed for opam packages.

That's all you need for `master` ```diff diff --git a/plugin/src/ast_plugin.ml4 b/plugin/src/ast_plugin.ml4 index d2d93b2..697290b 100644 --- a/plugin/src/ast_plugin.ml4 +++ b/plugin/src/ast_plugin.ml4 @@ -3,7 +3,6 @@ DECLARE PLUGIN "ast_plugin" open Format open Constr open...

I strongly suggest that plugins do follow the upstream branching scheme [which I do on my own projects] That is to say, `master` is supposed to work with the `master`...

Note that GitHub has a feature to set default branch shown on the main project page.

> The current code coincidentally compiles on Coq v8.9 even though it will crash when printing `Set` and has an extra wildcard after `Prop` (which OCaml warns about but allows)....

I confirm this PR fixes ocaml/opam#6129