Merge PR #11578: [exn] Keep information from multiple extra exn handlers

Reviewed-by: ppedrot

5 files changed, 11 insertions, 14 deletions

diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index 323dc8c1a4..a23cf3aaf1 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -79,7 +79,7 @@ let is_anomaly = function
 (** 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) =
+let register_additional_error_info (f : Exninfo.info -> (Pp.t Loc.located) option) =
   additional_error_info_handler := f :: !additional_error_info_handler
 
 (** [print_gen] is a general exception printer which tries successively
@@ -93,18 +93,15 @@ let rec print_gen ~anomaly ~extra_msg stk e =
   | h::stk' ->
     match h e with
     | Some err_msg ->
-      Option.cata (fun msg -> msg ++ err_msg) err_msg extra_msg
+      extra_msg ++ err_msg
     | None ->
       print_gen ~anomaly ~extra_msg stk' e
 
 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 = match extra_info with
-    | None -> None
-    | Some (loc, msg) -> msg
+  let extra_msg =
+    CList.map_filter (fun f -> f info) !additional_error_info_handler
+    (* Location info in the handler is ignored *)
+    |> List.map snd |> Pp.seq
   in
   try
     print_gen ~anomaly ~extra_msg !handle_stack e
diff --git a/lib/cErrors.mli b/lib/cErrors.mli
index ec81694177..f9c84b001c 100644
--- a/lib/cErrors.mli
+++ b/lib/cErrors.mli
@@ -75,5 +75,5 @@ val noncritical : exn -> bool
    exceptions. This method is fragile and should be considered
    deprecated *)
 val register_additional_error_info
-  :  (Exninfo.info -> (Pp.t option Loc.located) option)
+  :  (Exninfo.info -> Pp.t Loc.located option)
   -> unit
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 392f9b2ffd..3512bb936d 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -418,7 +418,7 @@ let extract_ltac_trace ?loc trace =
     (* We entered a user-defined tactic,
        we display the trace with location of the call *)
     let msg = hov 0 (explain_ltac_call_trace c tail loc ++ fnl()) in
-    (if Loc.finer loc tloc then loc else tloc), Some msg
+    (if Loc.finer loc tloc then loc else tloc), msg
   else
     (* We entered a primitive tactic, we don't display trace but
        report on the finest location *)
@@ -434,7 +434,7 @@ let extract_ltac_trace ?loc trace =
              aux best_loc tail
         | [] -> best_loc in
         aux loc trace in
-    best_loc, None
+    best_loc, mt ()
 
 let get_ltac_trace info =
   let ltac_trace = Exninfo.get info ltac_trace_info in
diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli
index e0126ad448..c76851a14c 100644
--- a/plugins/ltac/tactic_debug.mli
+++ b/plugins/ltac/tactic_debug.mli
@@ -79,4 +79,4 @@ val db_breakpoint : debug_info ->
   lident message_token list -> unit Proofview.NonLogical.t
 
 val extract_ltac_trace :
-  ?loc:Loc.t -> Tacexpr.ltac_trace -> Pp.t option Loc.located
+  ?loc:Loc.t -> Tacexpr.ltac_trace -> Pp.t Loc.located
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index 2a0c109a42..2820d3e3ad 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -862,7 +862,7 @@ let () = CErrors.register_additional_error_info begin fun info ->
     let bt =
       str "Backtrace:" ++ fnl () ++ prlist_with_sep fnl pr_frame bt ++ fnl ()
     in
-    Some (Loc.tag @@ Some bt)
+    Some (Loc.tag bt)
   else None
 end