Q_TAC

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

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

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.

See also

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