The Fail command does not catch uncaught exception anomalies anymore.

5 files changed, 23 insertions, 3 deletions

diff --git a/lib/errors.ml b/lib/errors.ml
index 999d99ee08..c60442654a 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -120,3 +120,12 @@ let noncritical = function
   | Timeout | Drop | Quit -> false
   | Invalid_argument "equal: functional value" -> false
   | _ -> true
+
+(** Check whether an exception is handled *)
+
+exception Bottom
+
+let handled e =
+  let bottom _ = raise Bottom in
+  try let _ = print_gen bottom !handle_stack e in true
+  with Bottom -> false
diff --git a/lib/errors.mli b/lib/errors.mli
index 5bd5724746..8320ce409f 100644
--- a/lib/errors.mli
+++ b/lib/errors.mli
@@ -88,3 +88,7 @@ val iprint_no_report : Exninfo.iexn -> Pp.std_ppcmds
     Typical example: [Sys.Break], [Assert_failure], [Anomaly] ...
 *)
 val noncritical : exn -> bool
+
+(** Check whether an exception is handled by some toplevel printer. The
+    [Anomaly] exception is never handled. *)
+val handled : exn -> bool
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index a0892bed9a..accba3121b 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -110,9 +110,16 @@ let rec strip_wrapping_exceptions = function
     strip_wrapping_exceptions e
   | exc -> exc
 
-let process_vernac_interp_error ?(with_header=true) (exc, info) =
+let process_vernac_interp_error ?(allow_uncaught=true) ?(with_header=true) (exc, info) =
   let exc = strip_wrapping_exceptions exc in
   let e = process_vernac_interp_error with_header (exc, info) in
+  let () =
+    if not allow_uncaught && not (Errors.handled (fst e)) then
+      let (e, info) = e in
+      let msg = str "Uncaught exception " ++ str (Printexc.to_string e) in
+      let err = Errors.make_anomaly msg in
+      Util.iraise (err, info)
+  in
   let ltac_trace = Exninfo.get info Proof_type.ltac_trace_info in
   let loc = Option.default Loc.ghost (Loc.get_loc info) in
   match ltac_trace with
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index 100b3772cc..729686f32d 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.mli
@@ -12,7 +12,7 @@ val print_loc : Loc.t -> Pp.std_ppcmds
 
 (** Pre-explain a vernac interpretation error *)
 
-val process_vernac_interp_error : ?with_header:bool -> Util.iexn -> Util.iexn
+val process_vernac_interp_error : ?allow_uncaught:bool -> ?with_header:bool -> Util.iexn -> Util.iexn
 
 (** General explain function. Should not be used directly now,
     see instead function [Errors.print] and variants *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 9d5edc80a0..849b1d47d6 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -2106,7 +2106,7 @@ let with_fail b f =
            | e ->
               let e = Errors.push e in
               raise (HasFailed (Errors.iprint
-                (Cerrors.process_vernac_interp_error ~with_header:false e))))
+                (Cerrors.process_vernac_interp_error ~allow_uncaught:false ~with_header:false e))))
         ()
     with e when Errors.noncritical e -> 
       let (e, _) = Errors.push e in