2 files changed, 5 insertions, 23 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 **)
 
diff --git a/lib/cErrors.mli b/lib/cErrors.mli
index 100dcd0b22..02eaf6bd0b 100644
--- a/lib/cErrors.mli
+++ b/lib/cErrors.mli
@@ -21,9 +21,6 @@ val push : exn -> Exninfo.iexn
  [Anomaly] is used for system errors and [UserError] for the
    user's ones. *)
 
-val make_anomaly : ?label:string -> Pp.t -> exn
-(** Create an anomaly. *)
-
 val anomaly : ?loc:Loc.t -> ?label:string -> Pp.t -> 'a
 (** Raise an anomaly, with an optional location and an optional
     label identifying the anomaly. *)
@@ -41,14 +38,6 @@ val user_err : ?loc:Loc.t -> ?hdr:string -> Pp.t -> 'a
 (** Main error raising primitive. [user_err ?loc ?hdr pp] signals an
     error [pp] with optional header and location [hdr] [loc] *)
 
-val invalid_arg : ?loc:Loc.t -> string -> 'a
-
-(** [todo] is for running of an incomplete code its implementation is
-   "do nothing" (or print a message), but this function should not be
-   used in a released code *)
-
-val todo : string -> unit
-
 exception Timeout
 
 (** [register_handler h] registers [h] as a handler.
@@ -72,7 +61,7 @@ exception Unhandled
 val register_handler : (exn -> Pp.t) -> unit
 
 (** The standard exception printer *)
-val print : ?info:Exninfo.info -> exn -> Pp.t
+val print : exn -> Pp.t
 val iprint : Exninfo.iexn -> Pp.t
 
 (** Same as [print], except that the "Please report" part of an anomaly