CHANGED_TAC : tactic -> tactic
SYNOPSIS
Makes a tactic fail if it has no effect.
DESCRIPTION
When applied to a tactic
t
, the tactical
CHANGED_TAC
gives a new tactic which is the same as
t
if that has any effect, and otherwise fails.
FAILURE CONDITIONS
The application of
CHANGED_TAC
to a tactic never fails. The resulting tactic fails if the basic tactic either fails or has no effect.
USES
Occasionally useful in controlling complicated tactic compositions. Also sometimes convenient just to check that a step did indeed modify a goal.
SEE ALSO
TRY
,
VALID
.