search

coq / vscoq

Visual Studio Code extension for Coq
MIT License
335 stars 68 forks source link

Hover on qualifed names #884

Closed ybertot closed 4 weeks ago

ybertot commented 1 month ago

In a window with the following contents:

Module sandbox.

Lemma Earth_shadowing_result : 2 + 2 = 4.
Proof. reflexivity. Qed.

End sandbox.

Lemma unqualified_name : 2 + 2 = 4.
Proof. exact sandbox.Earth_shadowing_result. Qed.

Lemma simple_corollary : 2 <= 4.
Proof.
rewrite <- unqualified_name.

When hovering with the mouse on the theorem name "sandbox.Earth_shadowing_result" (8th line) no extra information is displayed. When hovering with the mouse on the name unqualified_name, the type of this theorem appears. The first hovering result should be the same as the second one.

Durbatuluk1701 commented 1 month ago

I might also mention that along the same line, hover on a name that includes a single quote ' is broken: Image