Merge PR #9686: [error] Remove special error printing pre-processing

Reviewed-by: SkySkimmer

21 files changed, 165 insertions, 270 deletions

diff --git a/dev/base_include b/dev/base_include
index b30bbaa3fa..4841db8953 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -134,7 +134,6 @@ open Tacticals
 open Tactics
 open Eqschemes
 
-open ExplainErr
 open Class
 open ComDefinition
 open Indschemes
diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index 8406adfe18..3e1ba9107c 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -41,33 +41,6 @@ let invalid_arg ?loc s   = Loc.raise ?loc (Invalid_argument s)
 
 exception Timeout
 
-let handle_stack = ref []
-
-exception Unhandled
-
-let register_handler h = handle_stack := h::!handle_stack
-
-let is_handled e =
-  let is_handled_by h = (try let _ = h e in true with | Unhandled -> false) in
-  List.exists is_handled_by !handle_stack
-
-let is_anomaly = function
-| Anomaly _ -> true
-| exn -> not (is_handled exn)
-
-(** [print_gen] is a general exception printer which tries successively
-    all the handlers of a list, and finally a [bottom] handler if all
-    others have failed *)
-
-let rec print_gen bottom stk e =
-  match stk with
-  | [] -> bottom e
-  | h::stk' ->
-    try h e
-    with
-    | Unhandled -> print_gen bottom stk' e
-    | any -> print_gen bottom stk' any
-
 (** Only anomalies should reach the bottom of the handler stack.
     In usual situation, the [handle_stack] is treated as it if was always
     non-empty with [print_anomaly] as its bottom handler. *)
@@ -100,17 +73,67 @@ let print_anomaly askreport e =
   else
     hov 0 (raw_anomaly e)
 
+let handle_stack = ref []
+
+exception Unhandled
+
+let register_handler h = handle_stack := h::!handle_stack
+
+let is_handled e =
+  let is_handled_by h = (try let _ = h e in true with | Unhandled -> false) in
+  List.exists is_handled_by !handle_stack
+
+let is_anomaly = function
+| Anomaly _ -> true
+| exn -> not (is_handled exn)
+
+(** Printing of additional error info, from Exninfo *)
+let additional_error_info_handler = ref []
+
+let register_additional_error_info (f : Exninfo.info -> (Pp.t option Loc.located) option) =
+  additional_error_info_handler := f :: !additional_error_info_handler
+
+(** [print_gen] is a general exception printer which tries successively
+    all the handlers of a list, and finally a [bottom] handler if all
+    others have failed *)
+
+let rec print_gen ~anomaly ~extra_msg stk (e, info) =
+  match stk with
+  | [] ->
+    print_anomaly anomaly e
+  | h::stk' ->
+    try
+      let err_msg = h e in
+      Option.cata (fun msg -> msg ++ err_msg) err_msg extra_msg
+    with
+    | Unhandled -> print_gen ~anomaly ~extra_msg stk' (e,info)
+    | any -> print_gen ~anomaly ~extra_msg stk' (any,info)
+
+let print_gen ~anomaly (e, info) =
+  let extra_info =
+    try CList.find_map (fun f -> Some (f info)) !additional_error_info_handler
+    with Not_found -> None
+  in
+  let extra_msg, info = match extra_info with
+    | None -> None, info
+    | Some (loc, msg) ->
+      let info = Option.cata (fun l -> Loc.add_loc info l) info loc in
+      msg, info
+  in
+  print_gen ~anomaly ~extra_msg !handle_stack (e,info)
+
 (** The standard exception printer *)
-let print ?(info = Exninfo.null) e =
-  print_gen (print_anomaly true) !handle_stack e ++ print_backtrace info
+let print ?info e =
+  let info = Option.default Exninfo.(info e) info in
+  print_gen ~anomaly:true (e,info) ++ print_backtrace info
 
 let iprint (e, info) = print ~info e
 
 (** Same as [print], except that the "Please report" part of an anomaly
     isn't printed (used in Ltac debugging). *)
-let print_no_report e = print_gen (print_anomaly false) !handle_stack e
+let print_no_report e = print_gen ~anomaly:false (e, Exninfo.info e)
 let iprint_no_report (e, info) =
-  print_gen (print_anomaly false) !handle_stack e ++ print_backtrace info
+  print_gen ~anomaly:false (e,info) ++ print_backtrace info
 
 (** Predefined handlers **)
 
diff --git a/lib/cErrors.mli b/lib/cErrors.mli
index 8580622095..100dcd0b22 100644
--- a/lib/cErrors.mli
+++ b/lib/cErrors.mli
@@ -86,3 +86,10 @@ val iprint_no_report : Exninfo.iexn -> Pp.t
     Typical example: [Sys.Break], [Assert_failure], [Anomaly] ...
 *)
 val noncritical : exn -> bool
+
+(** Register a printer for errors carrying additional information on
+   exceptions. This method is fragile and should be considered
+   deprecated *)
+val register_additional_error_info
+  :  (Exninfo.info -> (Pp.t option Loc.located) option)
+  -> unit
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index bf2b4c9122..0efb27e3f0 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -79,7 +79,7 @@ let do_observe_tac s tac g =
   with reraise ->
     let reraise = CErrors.push reraise in
     if not (Stack.is_empty debug_queue)
-    then print_debug_queue (Some (fst (ExplainErr.process_vernac_interp_error reraise)));
+    then print_debug_queue (Some (fst reraise));
     iraise reraise
 
 let observe_tac_stream s tac g =
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index e20d010c71..5f859b3e4b 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -227,7 +227,6 @@ END
 {
 
 let warning_error names e =
-  let (e, _) = ExplainErr.process_vernac_interp_error (e, Exninfo.null) in
   match e with
     | Building_graph e ->
        let names = pr_enum Libnames.pr_qualid names in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 9a9e0b9692..48e3129599 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -244,9 +244,6 @@ let prepare_body ((name,_,args,types,_),_) rt =
   let fun_args,rt' = chop_rlambda_n n rt in
   (fun_args,rt')
 
-let process_vernac_interp_error e =
-  fst (ExplainErr.process_vernac_interp_error (e, Exninfo.null))
-
 let warn_funind_cannot_build_inversion =
   CWarnings.create ~name:"funind-cannot-build-inversion" ~category:"funind"
     (fun e' -> strbrk "Cannot build inversion information" ++
@@ -293,11 +290,9 @@ let derive_inversion fix_names =
         fix_names_as_constant
         lind;
       with e when CErrors.noncritical e ->
-      let e' = process_vernac_interp_error e in
-      warn_funind_cannot_build_inversion e'
+        warn_funind_cannot_build_inversion e
   with e when CErrors.noncritical e ->
-    let e' = process_vernac_interp_error e in
-    warn_funind_cannot_build_inversion e'
+    warn_funind_cannot_build_inversion e
 
 let warn_cannot_define_graph =
   CWarnings.create ~name:"funind-cannot-define-graph" ~category:"funind"
@@ -310,17 +305,13 @@ let warn_cannot_define_principle =
       h 1 names ++ error)
 
 let warning_error names e =
-  let e = process_vernac_interp_error e in
   let e_explain e =
     match e with
       | ToShow e ->
-        let e = process_vernac_interp_error e in
         spc () ++ CErrors.print e
       | _ ->
         if do_observe ()
-        then
-          let e = process_vernac_interp_error e in
-          (spc () ++ CErrors.print e)
+        then (spc () ++ CErrors.print e)
         else mt ()
   in
   match e with
@@ -333,7 +324,6 @@ let warning_error names e =
     | _ -> raise e
 
 let error_error names e =
-  let e = process_vernac_interp_error e in
   let e_explain e =
     match e with
       | ToShow e -> spc () ++ CErrors.print e
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 549f6d42c9..8fa001278b 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -54,9 +54,8 @@ let do_observe_tac s tac g =
     msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v
   with reraise ->
     let reraise = CErrors.push reraise in
-    let e = ExplainErr.process_vernac_interp_error reraise in
     observe (hov 0 (str "observation "++ s++str " raised exception " ++
-             CErrors.iprint e ++ str " on goal" ++ fnl() ++ goal ));
+             CErrors.iprint reraise ++ str " on goal" ++ fnl() ++ goal ));
     iraise reraise;;
 
 let observe_tac s tac g =
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 8d6b85f94d..f4edbda04a 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -210,7 +210,7 @@ let print_debug_queue b e =
     begin
       let lmsg,goal = Stack.pop debug_queue in
       if b then
-        Feedback.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ CErrors.print e) ++ str " on goal" ++ fnl() ++ goal))
+        Feedback.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ CErrors.iprint e) ++ str " on goal" ++ fnl() ++ goal))
       else
         begin
           Feedback.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal));
@@ -237,7 +237,7 @@ let do_observe_tac s tac g =
   with reraise ->
     let reraise = CErrors.push reraise in
     if not (Stack.is_empty debug_queue)
-    then print_debug_queue true (fst (ExplainErr.process_vernac_interp_error reraise));
+    then print_debug_queue true reraise;
     iraise reraise
 
 let observe_tac s tac g =
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 3014ba5115..9e735e0680 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -33,12 +33,8 @@ type debug_info =
   | DebugOff
 
 (* An exception handler *)
-let explain_logic_error e =
-  CErrors.print (fst (ExplainErr.process_vernac_interp_error (e, Exninfo.null)))
-
-let explain_logic_error_no_anomaly e =
-  CErrors.print_no_report
-    (fst (ExplainErr.process_vernac_interp_error (e, Exninfo.null)))
+let explain_logic_error e = CErrors.print e
+let explain_logic_error_no_anomaly e = CErrors.print_no_report e
 
 let msg_tac_debug s = Proofview.NonLogical.print_debug (s++fnl())
 let msg_tac_notice s = Proofview.NonLogical.print_notice (s++fnl())
@@ -370,8 +366,9 @@ let explain_ltac_call_trace last trace loc =
           strbrk " (with " ++
             prlist_with_sep pr_comma
             (fun (id,c) ->
-              (* XXX: This hooks into the ExplainErr extension API
-                 so it is tricky to provide the right env for now. *)
+              (* XXX: This hooks into the CErrors's additional error
+                 info API so it is tricky to provide the right env for
+                 now. *)
               let env = Global.env () in
               let sigma = Evd.from_env env in
               Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders_env env sigma c)
@@ -424,11 +421,11 @@ let extract_ltac_trace ?loc trace =
         aux loc trace in
     best_loc, None
 
-let get_ltac_trace (_, info) =
+let get_ltac_trace info =
   let ltac_trace = Exninfo.get info ltac_trace_info in
   let loc = Loc.get_loc info in
   match ltac_trace with
   | None -> None
   | Some trace -> Some (extract_ltac_trace ?loc trace)
 
-let () = ExplainErr.register_additional_error_info get_ltac_trace
+let () = CErrors.register_additional_error_info get_ltac_trace
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 279e7ce1a6..0adabb0673 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -412,11 +412,10 @@ let interp_search_arg arg =
       if is_ident_part s then Search.GlobSearchString s else
       interp_search_notation ~loc s key
   | RGlobSearchSubPattern p ->
-      try
-        let env = Global.env () in
-        let _, p = Constrintern.intern_constr_pattern env (Evd.from_env env) p in
-        Search.GlobSearchSubPattern p
-      with e -> let e = CErrors.push e in iraise (ExplainErr.process_vernac_interp_error e)) arg in
+    let env = Global.env () in
+    let _, p = Constrintern.intern_constr_pattern env (Evd.from_env env) p in
+    Search.GlobSearchSubPattern p) arg
+  in
   let hpat, a1 = match arg with
   | (_, Search.GlobSearchSubPattern (Pattern.PMeta _)) :: a' -> all_true, a'
   | (true, Search.GlobSearchSubPattern p) :: a' ->
diff --git a/stm/stm.ml b/stm/stm.ml
index 4db4579e38..9bbff476f8 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -120,13 +120,12 @@ let call = get
 
 let call_process_error_once =
   let processed : unit Exninfo.t = Exninfo.make () in
-  fun (_, info as ei) ->
+  fun (e, info) ->
     match Exninfo.get info processed with
-    | Some _ -> ei
+    | Some _ -> e, info
     | None ->
-        let e, info = ExplainErr.process_vernac_interp_error ei in
-        let info = Exninfo.add info processed () in
-        e, info
+      let info = Exninfo.add info processed () in
+      e, info
 
 end
 
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index 624d4d7f04..3b8fc58c6f 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -811,18 +811,18 @@ let () = register_handler begin function
 | _ -> raise Unhandled
 end
 
-let () = ExplainErr.register_additional_error_info begin fun (e, info) ->
+let () = CErrors.register_additional_error_info begin fun info ->
   if !Tac2interp.print_ltac2_backtrace then
     let bt = Exninfo.get info backtrace in
     let bt = match bt with
     | Some bt -> bt
-    | None -> raise Exit
+    | None -> []
     in
     let bt =
       str "Backtrace:" ++ fnl () ++ prlist_with_sep fnl pr_frame bt ++ fnl ()
     in
     Some (Loc.tag @@ Some bt)
-  else raise Exit
+  else None
 end
 
 (** Printing *)
diff --git a/user-contrib/Ltac2/tac2print.ml b/user-contrib/Ltac2/tac2print.ml
index b89067086f..1ece3d4242 100644
--- a/user-contrib/Ltac2/tac2print.ml
+++ b/user-contrib/Ltac2/tac2print.ml
@@ -473,8 +473,7 @@ end
 
 let () = register_init "err" begin fun _ _ e ->
   let e = to_ext val_exn e in
-  let (e, _) = ExplainErr.process_vernac_interp_error e in
-  str "err:(" ++ CErrors.print_no_report e ++ str ")"
+  str "err:(" ++ CErrors.iprint e ++ str ")"
 end
 
 let () =
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index a947fa2668..c7b8b13282 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -548,16 +548,11 @@ let obligation_terminator entries uctx { name; num; auto } =
         else ctx
     in
     let prg = {prg with prg_ctx} in
-    begin try
-      ignore (update_obls prg obls (pred rem));
-      if pred rem > 0 then
-        let deps = dependencies obls num in
-        if not (Int.Set.is_empty deps) then
-          ignore (auto (Some name) deps None)
-    with e when CErrors.noncritical e ->
-      let e = CErrors.push e in
-      pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e))
-    end
+    ignore (update_obls prg obls (pred rem));
+    if pred rem > 0 then
+      let deps = dependencies obls num in
+      if not (Int.Set.is_empty deps) then
+        ignore (auto (Some name) deps None)
   | _ ->
     CErrors.anomaly
       Pp.(
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
deleted file mode 100644
index ba1191285a..0000000000
--- a/vernac/explainErr.ml
+++ /dev/null
@@ -1,123 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Pp
-open CErrors
-open Type_errors
-open Pretype_errors
-open Indrec
-
-let guill s = str "\"" ++ str s ++ str "\""
-
-(** Invariant : exceptions embedded in EvaluatedError satisfy
-    Errors.noncritical *)
-
-exception EvaluatedError of Pp.t * exn option
-
-(** Registration of generic errors
-    Nota: explain_exn does NOT end with a newline anymore!
-*)
-
-let explain_exn_default = function
-  (* Basic interaction exceptions *)
-  | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".")
-  | CLexer.Error.E err -> hov 0 (str (CLexer.Error.to_string err))
-  | Sys_error msg -> hov 0 (str "System error: " ++ guill msg)
-  | Out_of_memory -> hov 0 (str "Out of memory.")
-  | Stack_overflow -> hov 0 (str "Stack overflow.")
-  | Dynlink.Error e -> hov 0 (str "Dynlink error: " ++ str Dynlink.(error_message e))
-  | Timeout -> hov 0 (str "Timeout!")
-  | Sys.Break -> hov 0 (fnl () ++ str "User interrupt.")
-  (* Exceptions with pre-evaluated error messages *)
-  | EvaluatedError (msg,None) -> msg
-  | EvaluatedError (msg,Some reraise) -> msg ++ CErrors.print reraise
-  (* Otherwise, not handled here *)
-  | _ -> raise CErrors.Unhandled
-
-let _ = CErrors.register_handler explain_exn_default
-
-
-let vernac_interp_error_handler = function
-  | Univ.UniverseInconsistency i ->
-    let msg =
-      if !Constrextern.print_universes then
-        str "." ++ spc() ++
-        Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i
-      else
-	mt() in
-    str "Universe inconsistency" ++ msg ++ str "."
-  | TypeError(ctx,te) ->
-    let te = map_ptype_error EConstr.of_constr te in
-    Himsg.explain_type_error ctx Evd.empty te
-  | PretypeError(ctx,sigma,te) ->
-    Himsg.explain_pretype_error ctx sigma te
-  | Notation.PrimTokenNotationError(kind,ctx,sigma,te) ->
-    Himsg.explain_prim_token_notation_error kind ctx sigma te
-  | Typeclasses_errors.TypeClassError(env, sigma, te) ->
-    Himsg.explain_typeclass_error env sigma te
-  | InductiveError e ->
-    Himsg.explain_inductive_error e
-  | Modops.ModuleTypingError e ->
-    Himsg.explain_module_error e
-  | Modintern.ModuleInternalizationError e ->
-    Himsg.explain_module_internalization_error e
-  | RecursionSchemeError (env,e) ->
-    Himsg.explain_recursion_scheme_error env e
-  | Cases.PatternMatchingError (env,sigma,e) ->
-    Himsg.explain_pattern_matching_error env sigma e
-  | Tacred.ReductionTacticError e ->
-    Himsg.explain_reduction_tactic_error e
-  | Logic.RefinerError (env, sigma, e) ->
-    Himsg.explain_refiner_error env sigma e
-  | Nametab.GlobalizationError q ->
-    str "The reference" ++ spc () ++ Libnames.pr_qualid q ++
-    spc () ++ str "was not found" ++
-    spc () ++ str "in the current" ++ spc () ++ str "environment."
-  | Refiner.FailError (i,s) ->
-    let s = Lazy.force s in
-    str "Tactic failure" ++
-    (if Pp.ismt s then s else str ": " ++ s) ++
-    if Int.equal i 0 then str "." else str " (level " ++ int i ++ str")."
-  | _ ->
-    raise CErrors.Unhandled
-
-let _ = CErrors.register_handler vernac_interp_error_handler
-
-(** Pre-explain a vernac interpretation error *)
-
-let wrap_vernac_error (exn, info) strm = (EvaluatedError (strm, None), info)
-
-let process_vernac_interp_error exn =
-  try vernac_interp_error_handler (fst exn) |> wrap_vernac_error exn
-  with CErrors.Unhandled -> exn
-
-let rec strip_wrapping_exceptions = function
-  | Logic_monad.TacticFailure e ->
-    strip_wrapping_exceptions e
-  | exc -> exc
-
-let additional_error_info = ref []
-
-let register_additional_error_info f =
-  additional_error_info := f :: !additional_error_info
-
-let process_vernac_interp_error (exc, info) =
-  let exc = strip_wrapping_exceptions exc in
-  let e = process_vernac_interp_error (exc, info) in
-  let e' =
-    try Some (CList.find_map (fun f -> f e) !additional_error_info)
-    with _ -> None
-  in
-  let add_loc_opt ?loc info = Option.cata (fun l -> Loc.add_loc info l) info loc in
-  match e' with
-  | None -> e
-  | Some (loc, None) -> (fst e, add_loc_opt ?loc (snd e))
-  | Some (loc, Some msg) ->
-    (EvaluatedError (msg, Some (fst e)), add_loc_opt ?loc (snd e))
diff --git a/vernac/explainErr.mli b/vernac/explainErr.mli
deleted file mode 100644
index cc2a130925..0000000000
--- a/vernac/explainErr.mli
+++ /dev/null
@@ -1,23 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(** Toplevel Exception *)
-exception EvaluatedError of Pp.t * exn option
-
-(** Pre-explain a vernac interpretation error *)
-
-val process_vernac_interp_error : Util.iexn -> Util.iexn
-
-(** General explain function. Should not be used directly now,
-    see instead function [Errors.print] and variants *)
-
-val explain_exn_default : exn -> Pp.t
-
-val register_additional_error_info : (Util.iexn -> (Pp.t option Loc.located) option) -> unit
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 2e218942cb..ea34b601e8 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -1353,3 +1353,70 @@ let explain_prim_token_notation_error kind env sigma = function
     (strbrk "Unexpected non-option term " ++
      pr_constr_env env sigma c ++
      strbrk (" while parsing a "^kind^" notation."))
+
+(** Registration of generic errors
+    Nota: explain_exn does NOT end with a newline anymore!
+*)
+
+let explain_exn_default = function
+  (* Basic interaction exceptions *)
+  | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".")
+  | CLexer.Error.E err -> hov 0 (str (CLexer.Error.to_string err))
+  | Sys_error msg -> hov 0 (str "System error: " ++ quote (str msg))
+  | Out_of_memory -> hov 0 (str "Out of memory.")
+  | Stack_overflow -> hov 0 (str "Stack overflow.")
+  | Dynlink.Error e -> hov 0 (str "Dynlink error: " ++ str Dynlink.(error_message e))
+  | CErrors.Timeout -> hov 0 (str "Timeout!")
+  | Sys.Break -> hov 0 (fnl () ++ str "User interrupt.")
+  (* Otherwise, not handled here *)
+  | _ -> raise CErrors.Unhandled
+
+let _ = CErrors.register_handler explain_exn_default
+
+let rec vernac_interp_error_handler = function
+  | Univ.UniverseInconsistency i ->
+    let msg =
+      if !Constrextern.print_universes then
+        str "." ++ spc() ++
+        Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i
+      else
+        mt() in
+    str "Universe inconsistency" ++ msg ++ str "."
+  | TypeError(ctx,te) ->
+    let te = map_ptype_error EConstr.of_constr te in
+    explain_type_error ctx Evd.empty te
+  | PretypeError(ctx,sigma,te) ->
+    explain_pretype_error ctx sigma te
+  | Notation.PrimTokenNotationError(kind,ctx,sigma,te) ->
+    explain_prim_token_notation_error kind ctx sigma te
+  | Typeclasses_errors.TypeClassError(env, sigma, te) ->
+    explain_typeclass_error env sigma te
+  | InductiveError e ->
+    explain_inductive_error e
+  | Modops.ModuleTypingError e ->
+    explain_module_error e
+  | Modintern.ModuleInternalizationError e ->
+    explain_module_internalization_error e
+  | RecursionSchemeError (env,e) ->
+    explain_recursion_scheme_error env e
+  | Cases.PatternMatchingError (env,sigma,e) ->
+    explain_pattern_matching_error env sigma e
+  | Tacred.ReductionTacticError e ->
+    explain_reduction_tactic_error e
+  | Logic.RefinerError (env, sigma, e) ->
+    explain_refiner_error env sigma e
+  | Nametab.GlobalizationError q ->
+    str "The reference" ++ spc () ++ Libnames.pr_qualid q ++
+    spc () ++ str "was not found" ++
+    spc () ++ str "in the current" ++ spc () ++ str "environment."
+  | Refiner.FailError (i,s) ->
+    let s = Lazy.force s in
+    str "Tactic failure" ++
+    (if Pp.ismt s then s else str ": " ++ s) ++
+    if Int.equal i 0 then str "." else str " (level " ++ int i ++ str")."
+  | Logic_monad.TacticFailure e ->
+    vernac_interp_error_handler e
+  | _ ->
+    raise CErrors.Unhandled
+
+let _ = CErrors.register_handler vernac_interp_error_handler
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index 6458fb9e30..9de5284393 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -8,37 +8,11 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Environ
-open Type_errors
-open Pretype_errors
-open Typeclasses_errors
-open Indrec
-open Cases
-open Logic
-
 (** This module provides functions to explain the type errors. *)
 
-val explain_type_error : env -> Evd.evar_map -> type_error -> Pp.t
-
-val explain_pretype_error : env -> Evd.evar_map -> pretype_error -> Pp.t
-
-val explain_inductive_error : inductive_error -> Pp.t
-
-val explain_typeclass_error : env -> Evd.evar_map -> typeclass_error -> Pp.t
-
-val explain_recursion_scheme_error : env -> recursion_scheme_error -> Pp.t
-
-val explain_refiner_error : env -> Evd.evar_map -> refiner_error -> Pp.t
-
-val explain_pattern_matching_error :
-  env -> Evd.evar_map -> pattern_matching_error -> Pp.t
-
-val explain_reduction_tactic_error :
-  Tacred.reduction_tactic_error -> Pp.t
-
-val explain_module_error : Modops.module_typing_error -> Pp.t
+(* Used by equations *)
+val explain_type_error : Environ.env -> Evd.evar_map -> Pretype_errors.type_error -> Pp.t
 
-val explain_module_internalization_error :
-  Modintern.module_internalization_error -> Pp.t
+val explain_pretype_error : Environ.env -> Evd.evar_map -> Pretype_errors.pretype_error -> Pp.t
 
-val explain_prim_token_notation_error : string -> env -> Evd.evar_map -> Notation.prim_token_notation_error -> Pp.t
+val explain_refiner_error : Environ.env -> Evd.evar_map -> Logic.refiner_error -> Pp.t
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 5d7e1ff9f6..eb1e3b74b4 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -467,12 +467,7 @@ let obligation_hook prg obl num auto { DeclareDef.Hook.S.uctx = ctx'; dref; _ }
   let obls = Array.copy obls in
   let () = obls.(num) <- obl in
   let prg = { prg with prg_ctx = ctx' } in
-  let () =
-    try ignore (update_obls prg obls (pred rem))
-    with e when CErrors.noncritical e ->
-      let e = CErrors.push e in
-      pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e))
-  in
+  let () = ignore (update_obls prg obls (pred rem)) in
   if pred rem > 0 then begin
     let deps = dependencies obls num in
     if not (Int.Set.is_empty deps) then
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index d28eeb341d..4def1d78af 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -5,7 +5,6 @@ G_vernac
 G_proofs
 Vernacprop
 Himsg
-ExplainErr
 Locality
 Egramml
 Vernacextend
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 681605cc31..255283ba36 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2233,7 +2233,7 @@ let with_fail f : (Pp.t, unit) result =
   (* Fail Timeout is a common pattern so we need to support it. *)
   | e when CErrors.noncritical e || e = Timeout ->
     (* The error has to be printed in the failing state *)
-    Ok CErrors.(iprint ExplainErr.(process_vernac_interp_error (push e)))
+    Ok CErrors.(iprint (push e))
 
 (* We restore the state always *)
 let with_fail ~st f =