-(* let thens ~start ~continuations =
- let thens ~start ~continuations status =
- let output_status = S.apply_tactic start status in
- let new_goals = S.goals output_status in
- try
- let output_status,goals =
- List.fold_left2
- (fun (output_status,goals) goal tactic ->
- let status = S.focus goal output_status in
- let output_status' = S.apply_tactic tactic status in
- let new_goals' = S.goals output_status' in
- (output_status',goals@new_goals')
- ) (output_status,[]) new_goals continuations
- in
- S.set_goals output_status goals
- with
- Invalid_argument _ ->
- let debug = Printf.sprintf "thens: expected %i new goals, found %i"
- (List.length continuations) (List.length new_goals)
- in
- raise (Fail debug)
- in
- S.mk_tactic (thens ~start ~continuations ) *)
-