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