Emilio Jesús Gallego Arias

> I think the solution I'm imagining is that there's an annotation whose default value is "on for definitions and fixpoints not in proof mode, off for proof mode", so...

Still on master: ``` Error: Anomaly "in retyping: Non-functional construction." Please report at http://coq.inria.fr/bugs/. Raised at Exninfo.iraise in file "clib/exninfo.ml", line 80, characters 4-11 Called from Unification.unify_to_type in file "pretyping/unification.ml",...

@andres-erbsen what's the problem here? We build Coq without GTK in our CI, and it works fine.

Oh, I was not aware that target was removed, I'm unsure when that happened. The only change that needs to be done in the Makefile is to remove `coqide.install` from...

Maybe; tho note that `world` target is pretty old in the Coq world, so any change of semantics will likely create some problems to users. Maybe `world-noide`? Also our default...

Yup, but that was a kind of misfeature for regular developers, in the sense that it is hard to guess the intention of the developer, and incomplete builds due to...

@Alizter what's the status of this in your test-suite branch?

Actually I was going to run this PR with my infra to report leaks, would be indeed great if we could repair this at some point

I am not sure this bug still applies? IIANM `cd` should not affect the .vo output path anymore. Only use case for `Cd` I think is extraction, we could indeed...

@herbelin would it make more sense to allow UIs to show this on hover? We can easily hack this for coq-lsp if you would like to.