RENAME1_TAC
Q.RENAME1_TAC : term quotation -> tactic
Finds an instance of a pattern in a goal, and renames to use names from the pattern.
The tactic Q.RENAME1_TAC q is defined to be
MATCH_RENAME_TAC q ORELSE MATCH_ASSUM_RENAME_TAC q ORELSE
MATCH_GOALSUB_RENAME_TAC q ORELSE MATCH_ASMSUB_RENAME_TAC q
Failure
Fails if all of the constituent tactics fail.
Comments
This tactic can be used to force a particular set of names on a goal,
hopefully making the resulting tactic more robust in the face of
underlying implementation changes. Note though that successful use of
this tactic requires that the "new" names in the provided pattern really
be fresh for the goal. If one is really uncertain about what names might
be appearing in a goal, this condition may be difficult to ensure,
particularly as the tactic only looks for one instance of the pattern at
a time (but see Q.RENAME_TAC).
This tactic is also available under the alias bossLib.rename1.
See also
Q.MATCH_ASMSUB_RENAME_TAC,
Q.MATCH_ASSUM_RENAME_TAC,
Q.MATCH_GOALSUB_RENAME_TAC,
Q.MATCH_RENAME_TAC