-
Robbert Krebbers authored
iSpecialize and iDestruct. These tactics now all take an iTrm, which is a tuple consisting of a.) a lemma or name of a hypotheses b.) arguments to instantiate c.) a specialization pattern.
5b224d9c
iSpecialize and iDestruct. These tactics now all take an iTrm, which is a tuple consisting of a.) a lemma or name of a hypotheses b.) arguments to instantiate c.) a specialization pattern.