coq-lsp icon indicating copy to clipboard operation
coq-lsp copied to clipboard

Published 20 hours ago • verified publisher icon ejgallego

autocomplete for hint databases

Open Alizter opened this issue 9 months ago • 1 comments

Many vernacular commands require a hint database. For instance,

Hint Immediate foo : typeclass_instances.

It would be nice if when we type : the autocompletion gave the names of hint databases available. This should be something we can easily look up and present to the user.

Alizter avatar Feb 11 '25 07:02 Alizter

I am not sure Coq's API does expose this list tho.

ejgallego avatar Feb 13 '25 13:02 ejgallego