+ (* Higher order tactics *)
+ | Do (_, count, tac) ->
+ Printf.sprintf "do %d %s" count (pp_tactic tac)
+ | Repeat (_, tac) -> "repeat " ^ pp_tactic tac
+ | Seq (_, tacs) -> pp_tactics ~sep:"; " tacs
+ | Then (_, tac, tacs) ->
+ Printf.sprintf "%s; [%s]" (pp_tactic tac)
+ (pp_tactics ~sep:" | " tacs)
+ | First (_, tacs) ->
+ Printf.sprintf "tries [%s]" (pp_tactics ~sep:" | " tacs)
+ | Try (_, tac) -> "try " ^ pp_tactic tac
+ | Solve (_, tac) ->
+ Printf.sprintf "solve [%s]" (pp_tactics ~sep:" | " tac)
+ | Progress (_, tac) -> "progress " ^ pp_tactic tac
+ (* First order tactics *)