----------------------------------------------------------------------
RENAME1_TAC                                                        (Q)
----------------------------------------------------------------------
RENAME1_TAC : term quotation -> tactic

SYNOPSIS
Finds an instance of a pattern in a goal, and renames to use names
from the pattern.

KEYWORDS


DESCRIBE
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}.

SEEALSO
Q.MATCH_ASMSUB_RENAME_TAC, Q.MATCH_ASSUM_RENAME_TAC,
Q.MATCH_GOALSUB_RENAME_TAC, Q.MATCH_RENAME_TAC.

----------------------------------------------------------------------