Emilio Jesús Gallego Arias

Note also https://github.com/coq/coq/pull/16505 , before this, we had `(optional)` in coqide as to try to handle the case of missing lablgtk better. But as you can see this stuff is...

I still think it is a good idea to go ahead with this, wdyt @SkySkimmer ?

Ok

Indeed it seems to me that this is a real problem and that we can do much better on the Coq side; there is a clear difference IMHO in terms...

The thing is that we already do a lot of hashconsing in Coq, so typing could for sure try to profit from it. Coq was never built with incrementality in...

I am not expert but @fpottier 's comment makes sense to me. Should we re-open this bug, or write a new one with a clear spec w.r.t. loss of sharing...

`coq/ast.ml` needs fixing I think!

Indeed, this is a PITA; it is easy to try different approaches tho with the current server tho. I tried a few myself, like sending the outline if on-demand has...

While I can fully understand the motivations, the new semantics for `Undo` are a bit weird. Reading the docs it is not clear to me what the difference between `Undo`...

> It shouldn't be new, it now treats `Fail whatever` like it always treated `Check whatever` Yes. Sorry I wasn't clear. My question is more, what are the differences between...