NULL_OK_LT
Tactical.NULL_OK_LT : list_tactic -> list_tactic
Makes a list-tactic succeed with no effect when applied to the empty goal list.
For any list-tactic ltac, the application NULL_OK_LT ltac gives a
new list-tactic which has the same effect as ltac when applied to a
non-empty goal list. Applied to the empty goal list it succeeds with no
effect.
Failure
The application of NULL_OK_LT to a list-tactic ltac never fails. The
resulting list-tactic fails if applied to a non-empty goal list on which
ltac fails.