A fairly niche shortcoming, but Coq allows for a little bit more than ASCII in identifiers, which VSCoq doesn't seem to take into account. For instance in the following minimal file, hovering over Y gives information about it, but not in the case of Xᵒ.
Definition Xᵒ : nat := 0.
Definition Y : nat := 1.
(* In the following, vscoq gives feedback about Y but not Xᵒ *)
Goal Y + Xᵒ = 1.
A fairly niche shortcoming, but Coq allows for a little bit more than ASCII in identifiers, which VSCoq doesn't seem to take into account. For instance in the following minimal file, hovering over
Ygives information about it, but not in the case ofXᵒ.