Clément Pit-Claudel <clement....@gmail.com> writes: > 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?
You told me about this but I forgot, what kind of matching capabilities does the trie have? Note that Coq already a "quasi-trie", which allows for efficient prefix-matching, but I deem that far from enough. Cheers, E. _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
