diff options
Diffstat (limited to 'lib/cErrors.ml')
| -rw-r--r-- | lib/cErrors.ml | 19 |
1 files changed, 8 insertions, 11 deletions
diff --git a/lib/cErrors.ml b/lib/cErrors.ml index 323dc8c1a4..d1548ab12e 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 |