A tactical that parses in the context of a goal, a la the Q library.
DESCRIPTION
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.