diff options
| author | Emilio Jesus Gallego Arias | 2016-12-06 17:16:16 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-03-21 15:47:14 +0100 |
| commit | f0341076aa60a84177a6b46db0d8d50df220536b (patch) | |
| tree | 3dd3acd080d858e7b4d14ea31231b09c8ec74ec5 /lib/cErrors.mli | |
| parent | eb68e001f2ebbf09dc32c999e9c9b0f116c0a530 (diff) | |
[error] Move back fatal_error to toplevel
This reverts 4444768d3f4f9c4fcdd440f7ab902886bd8e2b09
(the mllib dependencies that should be surely tweaked more).
The logic for `fatal_error` has no place in `CErrors`, this is
coqtop-specific code.
What is more, a libobject caller should handle the exception correctly,
I fail to see why the fix was needed on the first place.
Diffstat (limited to 'lib/cErrors.mli')
| -rw-r--r-- | lib/cErrors.mli | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/lib/cErrors.mli b/lib/cErrors.mli index 5cffc725d9..0665a8ce73 100644 --- a/lib/cErrors.mli +++ b/lib/cErrors.mli @@ -98,8 +98,3 @@ val noncritical : exn -> bool (** Check whether an exception is handled by some toplevel printer. The [Anomaly] exception is never handled. *) val handled : exn -> bool - -(** Prints info which is either an error or - an anomaly and then exits with the appropriate - error code *) -val fatal_error : Pp.std_ppcmds -> bool -> 'a |