Emilio Jesús Gallego Arias

At some point we will get this feature as a side effect of some ongoing work in the parser, but it is very low priority for us now. > we'll...

I see, thanks. Is it feasible to make fontification use Coq-returned data (such as pairs of position / tag) ?

The way implicits work is a bit subtle. In SerAPI you can query for implicits with `(Query () (Implictits id))` but a bit more work is necessary in order to...

Duplicate of #179

Duplicate of #179

Duplicate of #180

Installing psutil 5.9.1 solved the issue too.

Indeed `make install` is not supported anymore, as the message indicates. (And it can't be fixed as we don't manage install at all ourselves now) The recommended sequence for packagers...

So indeed, to clarify what is going on, Coq's configure just now sets where `coqc` _does expect_ the stdlib to be present. The build now produces *.install files which can...

@Zimmi48 `-prefix` is taken by configure, but only set's the search path for coqlib, it doesn't affect install. So a contract you have is that you gotta pass the same...