diff options
| author | Pierre-Marie Pédrot | 2020-05-16 13:57:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-16 13:57:58 +0200 |
| commit | ebaaa7371c3a3548ccec1836621726f6d829858a (patch) | |
| tree | f5bfbfa5ad485e7c2f7b680de794b2005506bef9 /lib/cErrors.mli | |
| parent | 2111994285a21df662c232fa5acfd60e8a640795 (diff) | |
| parent | 8fd01b538c5b4ea58eecf8be07ab8115619cca4d (diff) | |
Merge PR #11566: [misc] Better preserve backtraces in several modules
Ack-by: SkySkimmer
Reviewed-by: ppedrot
Diffstat (limited to 'lib/cErrors.mli')
| -rw-r--r-- | lib/cErrors.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/cErrors.mli b/lib/cErrors.mli index 21d41c996d..cf1857cf04 100644 --- a/lib/cErrors.mli +++ b/lib/cErrors.mli @@ -21,7 +21,7 @@ val push : exn -> Exninfo.iexn [Anomaly] is used for system errors and [UserError] for the user's ones. *) -val anomaly : ?loc:Loc.t -> ?label:string -> Pp.t -> 'a +val anomaly : ?loc:Loc.t -> ?info:Exninfo.info -> ?label:string -> Pp.t -> 'a (** Raise an anomaly, with an optional location and an optional label identifying the anomaly. *) @@ -34,7 +34,7 @@ exception UserError of string option * Pp.t (** Main error signaling exception. It carries a header plus a pretty printing doc *) -val user_err : ?loc:Loc.t -> ?hdr:string -> Pp.t -> 'a +val user_err : ?loc:Loc.t -> ?info:Exninfo.info -> ?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] *) |
