ORELSE_LT
op Tactical.ORELSE_LT : list_tactic * list_tactic -> list_tactic
Applies first list-tactic, and if it fails, applies the second instead.
If ltac1 and ltac2 are list-tactics, ltac1 ORELSE_LT ltac2 is a
list-tactic which applies ltac1 to a goal list, and if it fails,
applies ltac2 to the goals.
Failure
The application of ORELSE_LT to a pair of list-tactics never fails.
The resulting list-tactic fails if both ltac1 and ltac2 fail when
applied to the relevant goals.