| First (_, tacs) -> sprintf "tries [%s]" (pp_tacticals ~sep:" | " tacs)
| Try (_, tac) -> "try " ^ pp_tactical ~term_pp ~lazy_term_pp tac
| Solve (_, tac) -> sprintf "solve [%s]" (pp_tacticals ~sep:" | " tac)
| First (_, tacs) -> sprintf "tries [%s]" (pp_tacticals ~sep:" | " tacs)
| Try (_, tac) -> "try " ^ pp_tactical ~term_pp ~lazy_term_pp tac
| Solve (_, tac) -> sprintf "solve [%s]" (pp_tacticals ~sep:" | " tac)