- | Tactic (_, tac) -> pp_tactic tac
- | Do (_, count, tac) ->
- sprintf "do %d %s" count (pp_tactical ~term_pp ~lazy_term_pp tac)
- | Repeat (_, tac) -> "repeat " ^ pp_tactical ~term_pp ~lazy_term_pp tac
- | Seq (_, tacs) -> pp_tacticals ~sep:"; " tacs
- | Then (_, tac, tacs) ->
- sprintf "%s; [%s]" (pp_tactical ~term_pp ~lazy_term_pp tac)
- (pp_tacticals ~sep:" | " tacs)
- | 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)
- | Progress (_, tac) -> "progress " ^ pp_tactical ~term_pp ~lazy_term_pp tac
-