[error] Remove special error printing pre-processing

We remove the special error printing pre-processing in favor of just
calling the standard printers.

Error printing has been a bit complex for a while due to an incomplete
migration to a new printing scheme based on registering exception
printers; this PR should alleviate that by completing the registration
approach.

After this cleanup, it should not be ever necessary for normal
functions to worry a lot about catching errors and re-raising them,
unless they have some very special needs.

This change also allows to consolidate the `explainErr` and `himsg`
modules into one, removing the need to export the error printing
functions. Ideally we would make the contents of `himsg` more
localized, but this can be done in a gradual way.

8 files changed, 78 insertions, 194 deletions

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 =