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

Reviewed-by: SkySkimmer

2 files changed, 4 insertions, 5 deletions

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 () =