More efficient hypothesis selection in tactic matching.
More efficient hypothesis selection in tactic matching.

Instead of reconstructing sublists of available hypotheses, we thread a set of
used hypotheses. This is not particularly clever algorithmically, but on real
lift examples this should be reasonable. Indeed, the number k of hyp patterns
in a match goal is typically small, so this will be O(n^k). Furthermore this
variant prevents reconstructing a map of hypotheses upfront so the cost is null
when no hypotheses are being selected.

Zimmi48/coq,ejgallego/coq,SkySkimmer/coq,ejgallego/coq,coq/coq,coq/coq,Zimmi48/coq,Zimmi48/coq,Zimmi48/coq,coq/coq,SkySkimmer/coq,SkySkimmer/coq,ejgallego/coq,SkySkimmer/coq,coq/coq,ejgallego/coq