On 2019-04-30 17:28, Emilio Jesús Gallego Arias wrote: > I guess that for Coq we will try to allow to plug custom indexers to the > namespace operations so they can use their indexing method of choice.
Yup, that's roughly how it works in F*-land: the IDE backend plugs in two functions, and populates its own view of the completion candidates.
signature.asc
Description: OpenPGP digital signature
_______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
