let fail_tac (proof,goal) =
let _, metasenv, _, _ = proof in
let _, _, _ = CicUtil.lookup_meta goal metasenv in
- raise (Fail "fail tactical")
+ raise (Fail (lazy "fail tactical"))
in
mk_tactic fail_tac
first ~tactics status
| _ -> raise e (* [e] must not be caught ; let's re-raise it *)
)
- | [] -> raise (Fail "first: no tactics left")
+ | [] -> raise (Fail (lazy "first: no tactics left"))
in
S.mk_tactic (first ~tactics)
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)
+ let debug = lazy (Printf.sprintf "thens: expected %i new goals, found %i"
+ (List.length continuations) (List.length new_goals))
in
raise (Fail debug)
in
Printexc.to_string e));
solve_tactics ~tactics status
)
- | [] -> raise (Fail "solve_tactics cannot solve the goal");
+ | [] -> raise (Fail (lazy "solve_tactics cannot solve the goal"));
S.apply_tactic S.id_tac status
in
S.mk_tactic (solve_tactics ~tactics)