----------------------------------------------------------------------
Q_TAC                                                       (Tactical)
----------------------------------------------------------------------
Q_TAC : (term -> tactic) -> term quotation -> tactic

SYNOPSIS
A tactical that parses in the context of a goal, a la the Q library.

KEYWORDS
tactical.

DESCRIBE
When applied to a term tactic {T} and a quotation {q}, the tactic
{Q_TAC T q} first parses the quotation {q} in the context of the goal
to yield the term {tm}, and then applies the tactic {T tm} to the goal.

FAILURE
The application of {Q_TAC} to a term tactic {T} and a quotation {q}
never fails. The resulting composite tactic {Q_TAC T q} fails when
applied to a goal if either {q} cannot be parsed, or {T tm} fails when
applied to the goal.

COMMENTS
Useful for avoiding decorating terms with type abbreviations.

SEEALSO
Tactical.EVERY, Tactical.FIRST, Tactical.ORELSE, Tactical.THEN,
Tactical.THEN1, Tactical.THENL.

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