+let thens ~start ~continuations ~status =
+ let (proof,new_goals) = start ~status in
+ try
+ List.fold_left2
+ (fun (proof,goals) goal tactic ->
+ let (proof',new_goals') = tactic ~status:(proof,goal) in
+ (proof',goals@new_goals')
+ ) (proof,[]) new_goals continuations
+ with
+ Invalid_argument _ -> raise (Fail "thens: wrong number of new goals")
+
+let id_tac ~status:(proof,goal) =
+ (proof,[goal])
+
+let status_of_single_goal_tactic_result =
+ function
+ proof,[goal] -> proof,goal
+ | _ ->
+ raise (Fail "status_of_single_goal_tactic_result: the tactic did not produce exactly a new goal")
+