TRY : (tactic -> tactic)
Makes a tactic have no effect rather than fail.
For any tactic
, the application
gives a new tactic which has the same effect as
if that succeeds, and otherwise has no effect.
The application of
to a tactic never fails. The resulting tactic never fails.