Emilio Jesús Gallego Arias

Thanks a lot for this case folks, I have a fix ready, I'm wondering if we could produce a simpler test case to put in coq-lsp test suite that doesn't...

I have tested this example with current `main` and I cannot reproduce anymore.

A good way to start this is to make a function `point:Point.t -> Coq.Ast.t -> Coq.Id.t option` I am now wondering how does hover work when there are multiple targets...

By the way type inference and checking the type of a constant are two very different things in Coq.

Likely we'd like type inference to be a code action on a selection (which is very easy to implement actually, in the binder-free case)

Thanks @herbelin , I thought that was a problem with the coq-lsp setup, but indeed it prints badly in Coq too, not only for numeric notations, also `min` is printed...

Yup, same for CoqIDE back to 8.15

@Alizter not sure about the tags here, but we are gonna need a way to classify a large number of issues / bugs that are really upstream. Actualy moving this...

> Did you mean to title it pull diagnostics? Yes, thanks!

Yes I noticed this, and it is annoying; not sure how to fix it without losing the very nice trigger for \alpha1 etc... symbols. Maybe the protocol allows us to...