Forked from
Iris / Iris
Source project has a limited visibility.
-
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.
Robbert Krebbers authorediSpecialize 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.