leanprover/verso

Double-hover

Closed this issue · 1 comments

nomeata commented

double-hover

If there is an error hover, maybe hide the ident hover?

david-christiansen commented

FIxed in 407c3bb - thanks!