Type inference on hover

[Alizter]

Just like OCaml LSP, we should have a way of hovering over document elements and getting back type information or in the case of ltac, perhaps some documentation.

In order to do this, we need to take the AST of the document and refine it further on query so that we can extract important information like galina terms. Afterwhich, we can pass to Check or About etc.

[ejgallego]

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 on the cursor. It seems that LSP doesn't support that right? (cc : @artagnon )

[ejgallego]

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

[ejgallego]

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)