diff options
Diffstat (limited to 'lib/errors.mli')
| -rw-r--r-- | lib/errors.mli | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/lib/errors.mli b/lib/errors.mli index 3e551e394c..5f230d4c3b 100644 --- a/lib/errors.mli +++ b/lib/errors.mli @@ -90,3 +90,10 @@ val print_no_report : exn -> Pp.std_ppcmds (** Same as [print], except that anomalies are not printed but re-raised (used for the Fail command) *) val print_no_anomaly : exn -> Pp.std_ppcmds + +(** Critical exceptions shouldn't be catched and ignored by mistake + by inner functions during a [vernacinterp]. They should be handled + only at the very end of interp, to be displayed to the user. + Typical example: [Sys.Break], [Assert_failure], [Anomaly] ... +*) +val noncritical : exn -> bool |