(proof',goals@new_goals')
) (proof,[]) new_goals continuations
with
- Invalid_argument _ -> raise (Fail "thens: wrong number of new goals")
+ Invalid_argument _ ->
+(* FG: more debugging information *)
+ let debug = Printf.sprintf "thens: expected %i new goals, found %i"
+ (List.length continuations) (List.length new_goals)
+ in
+ raise (Fail debug)
in
mk_tactic (thens ~start ~continuations )