diff options
| author | Emilio Jesus Gallego Arias | 2016-08-19 01:58:04 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2016-08-19 02:01:56 +0200 |
| commit | 543ee0c7ad43874c577416af9f2e5a94d7d1e4d3 (patch) | |
| tree | caf22d0e607ed9e0bf9ba64d76b4c2aebce63d5a /lib/cErrors.mli | |
| parent | de038270f72214b169d056642eb7144a79e6f126 (diff) | |
Remove errorlabstrm in favor of user_err
As noted by @ppedrot, the first is redundant. The patch is basically a renaming.
We didn't make the component optional yet, but this could happen in a
future patch.
Diffstat (limited to 'lib/cErrors.mli')
| -rw-r--r-- | lib/cErrors.mli | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/lib/cErrors.mli b/lib/cErrors.mli index 291c39b84f..ad17be393f 100644 --- a/lib/cErrors.mli +++ b/lib/cErrors.mli @@ -34,10 +34,13 @@ val is_anomaly : exn -> bool tricks with anomalies thanks to it. See rather [noncritical] below. *) exception UserError of string * std_ppcmds -val error : string -> 'a -val errorlabstrm : string -> std_ppcmds -> 'a val user_err : ?loc:Loc.t -> string -> std_ppcmds -> 'a +(** Main error raising primitive. [user_err ?loc c pp] signals an + error [pp] in component [c], with optional location [loc] *) + +val error : string -> 'a +(** [error s] just calls [user_error "_" (str s)] *) exception AlreadyDeclared of std_ppcmds val alreadydeclared : std_ppcmds -> 'a |