diff options
Diffstat (limited to 'lib/errors.ml')
| -rw-r--r-- | lib/errors.ml | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/lib/errors.ml b/lib/errors.ml index 92e5ac6423..27baf4314f 100644 --- a/lib/errors.ml +++ b/lib/errors.ml @@ -124,3 +124,13 @@ let _ = register_handler begin function | UserError(s,pps) -> hov 0 (str "Error: " ++ where (Some s) ++ pps) | _ -> raise Unhandled end + +(** 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. *) + +let noncritical = function + | Sys.Break | Out_of_memory | Stack_overflow + | Assert_failure _ | Match_failure _ | Anomaly _ + | Timeout | Drop | Quit -> false + | _ -> true |