[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.

7 files changed, 18 insertions, 34 deletions

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' ->