On 2019-04-30 12:00, Emilio Jesús Gallego Arias wrote: > [Barring the problem that Coq itself has terrible internal support for > completion as of today]
That's indeed a problem. In F* we used a fancy trie structure that gets updated every time an identifier is added to the context, and rolled back when reverting a segment. Maybe that would work for Coq too?
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
