Add [iSelect], and various tactics based on it
This MR adds the following tactics:
-
iSelect (pat)%I tac
calls the tactictac
with the name of the last hypothesis of the Iris context matchingpat
, -
iRename select (pat)%I into name
renames the last hypothesis of the Iris context matchingpat
intoname
, -
iDestruct select (pat)%I as ...
is similar toiDestruct
but it acts on the last hypothesis of the Iris context matchingpat
, -
iClear select (pat)%I
clears the last hypothesis of the Iris context matchingpat
, -
iRevert select (pat)%I
reverts the last hypothesis of the Iris context matchingpat
, -
iFrame select (pat)%I
cancels the last hypothesis of the Iris context matchingpat
.
Edited by Ralf Jung
Merge request reports
Activity
Please register or sign in to reply