diff options
| author | Emilio Jesus Gallego Arias | 2019-07-01 00:16:40 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-08 13:12:05 +0200 |
| commit | b372c0cf33681ef7e8ae3524987c5581fd3f92c0 (patch) | |
| tree | a7da4cf538f3a481995ad86bdd7aa18822bccf8b /lib/cErrors.ml | |
| parent | a5e4dd7faa23abd4a4ebe093076484d090a8a47e (diff) | |
[errors] Small cleanups and removal of dead code.
Diffstat (limited to 'lib/cErrors.ml')
| -rw-r--r-- | lib/cErrors.ml | 15 |
1 files changed, 4 insertions, 11 deletions
diff --git a/lib/cErrors.ml b/lib/cErrors.ml index 3e1ba9107c..b9735d0579 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -25,20 +25,13 @@ let _ = in Printexc.register_printer pr -let make_anomaly ?label pp = - Anomaly (label, pp) - let anomaly ?loc ?label pp = Loc.raise ?loc (Anomaly (label, pp)) exception UserError of string option * Pp.t (* User errors *) -let todo s = prerr_string ("TODO: "^s^"\n") - let user_err ?loc ?hdr strm = Loc.raise ?loc (UserError (hdr, strm)) -let invalid_arg ?loc s = Loc.raise ?loc (Invalid_argument s) - exception Timeout (** Only anomalies should reach the bottom of the handler stack. @@ -123,17 +116,17 @@ let print_gen ~anomaly (e, info) = print_gen ~anomaly ~extra_msg !handle_stack (e,info) (** The standard exception printer *) -let print ?info e = - let info = Option.default Exninfo.(info e) info in +let iprint (e, info) = print_gen ~anomaly:true (e,info) ++ print_backtrace info -let iprint (e, info) = print ~info e +let print e = + iprint (e, Exninfo.info e) (** Same as [print], except that the "Please report" part of an anomaly isn't printed (used in Ltac debugging). *) -let print_no_report e = print_gen ~anomaly:false (e, Exninfo.info e) let iprint_no_report (e, info) = print_gen ~anomaly:false (e,info) ++ print_backtrace info +let print_no_report e = iprint_no_report (e, Exninfo.info e) (** Predefined handlers **) |