Hover on proof name

[Alizter]

Observe the following on hover:

From Coq Require Import Prelude.
Axiom A : Type.
Axiom a : A.
Definition foo {n : nat} : A := a.
Definition foo' {n : nat} : A. Proof. apply a. Qed.
Definition foo'' {n : nat} : A. Proof. apply a. Defined.

• Hovering on foo gives the type of foo since it has meaning where we interpret it.
• Hovering on foo' and foo'' is empty.

I think we should be using the env at Defined or Qed for these kinds of hovers, rather than at that point in the document, so that users can see the type of a definition/lemma.

Hover has more information than is available in the written type in these cases, such as universe variables. It would make it easier to inspect definitions universe annotations without having to go to the end, write it and then hover.

This look-ahead should obviously only happen when inspecting the name of a Definition or Lemma etc.

[ejgallego]

That's a good idea, IMHO implementing #322 would be enough to implement this cleanly.