in
context, t, (C.Meta (newmeta,irl))
else
- raise (Fail "intro(s): not enough products or let-ins")
+ raise (Fail (lazy "intro(s): not enough products or let-ins"))
in
collect_context context howmany ty
apply_tac_verbose_with_subst ~term status
(* TODO cacciare anche altre eccezioni? *)
with
- | CicUnification.UnificationFailure msg ->
- raise (Fail (CicUnification.explain_error msg))
- | CicTypeChecker.TypeCheckerFailure _ as e ->
- raise (Fail (Printexc.to_string e))
+ | CicUnification.UnificationFailure msg
+ | CicTypeChecker.TypeCheckerFailure msg ->
+ raise (Fail msg)
(* ALB *)
let apply_tac_verbose ~term status =
apply_tac ~term status
(* TODO cacciare anche altre eccezioni? *)
with
- | CicUnification.UnificationFailure msg ->
- raise (Fail (CicUnification.explain_error msg))
- | CicTypeChecker.TypeCheckerFailure _ as e ->
- raise (Fail (Printexc.to_string e))
+ | CicUnification.UnificationFailure msg
+ | CicTypeChecker.TypeCheckerFailure msg ->
+ raise (Fail msg)
in
mk_tactic (apply_tac ~term)
(newproof, [])
end
else
- raise (Fail "The type of the provided term is not the one expected.")
+ raise (Fail (lazy "The type of the provided term is not the one expected."))
in
mk_tactic (exact_tac ~term)