aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/base_include1
-rw-r--r--lib/cErrors.ml85
-rw-r--r--lib/cErrors.mli7
-rw-r--r--plugins/funind/functional_principles_proofs.ml2
-rw-r--r--plugins/funind/g_indfun.mlg1
-rw-r--r--plugins/funind/indfun.ml16
-rw-r--r--plugins/funind/invfun.ml3
-rw-r--r--plugins/funind/recdef.ml4
-rw-r--r--plugins/ltac/tactic_debug.ml17
-rw-r--r--plugins/ssr/ssrvernac.mlg9
-rw-r--r--stm/stm.ml9
-rw-r--r--user-contrib/Ltac2/tac2entries.ml6
-rw-r--r--user-contrib/Ltac2/tac2print.ml3
-rw-r--r--vernac/declareObl.ml15
-rw-r--r--vernac/explainErr.ml123
-rw-r--r--vernac/explainErr.mli23
-rw-r--r--vernac/himsg.ml67
-rw-r--r--vernac/himsg.mli34
-rw-r--r--vernac/obligations.ml7
-rw-r--r--vernac/vernac.mllib1
-rw-r--r--vernac/vernacentries.ml2
21 files changed, 165 insertions, 270 deletions
diff --git a/dev/base_include b/dev/base_include
index b30bbaa3fa..4841db8953 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -134,7 +134,6 @@ open Tacticals
open Tactics
open Eqschemes
-open ExplainErr
open Class
open ComDefinition
open Indschemes
diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index 8406adfe18..3e1ba9107c 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -41,33 +41,6 @@ let invalid_arg ?loc s = Loc.raise ?loc (Invalid_argument s)
exception Timeout
-let handle_stack = ref []
-
-exception Unhandled
-
-let register_handler h = handle_stack := h::!handle_stack
-
-let is_handled e =
- let is_handled_by h = (try let _ = h e in true with | Unhandled -> false) in
- List.exists is_handled_by !handle_stack
-
-let is_anomaly = function
-| Anomaly _ -> true
-| exn -> not (is_handled exn)
-
-(** [print_gen] is a general exception printer which tries successively
- all the handlers of a list, and finally a [bottom] handler if all
- others have failed *)
-
-let rec print_gen bottom stk e =
- match stk with
- | [] -> bottom e
- | h::stk' ->
- try h e
- with
- | Unhandled -> print_gen bottom stk' e
- | any -> print_gen bottom stk' any
-
(** Only anomalies should reach the bottom of the handler stack.
In usual situation, the [handle_stack] is treated as it if was always
non-empty with [print_anomaly] as its bottom handler. *)
@@ -100,17 +73,67 @@ let print_anomaly askreport e =
else
hov 0 (raw_anomaly e)
+let handle_stack = ref []
+
+exception Unhandled
+
+let register_handler h = handle_stack := h::!handle_stack
+
+let is_handled e =
+ let is_handled_by h = (try let _ = h e in true with | Unhandled -> false) in
+ List.exists is_handled_by !handle_stack
+
+let is_anomaly = function
+| Anomaly _ -> true
+| exn -> not (is_handled exn)
+
+(** 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) =
+ additional_error_info_handler := f :: !additional_error_info_handler
+
+(** [print_gen] is a general exception printer which tries successively
+ all the handlers of a list, and finally a [bottom] handler if all
+ others have failed *)
+
+let rec print_gen ~anomaly ~extra_msg stk (e, info) =
+ match stk with
+ | [] ->
+ print_anomaly anomaly e
+ | h::stk' ->
+ try
+ let err_msg = h e in
+ Option.cata (fun msg -> msg ++ err_msg) err_msg extra_msg
+ with
+ | Unhandled -> print_gen ~anomaly ~extra_msg stk' (e,info)
+ | any -> print_gen ~anomaly ~extra_msg stk' (any,info)
+
+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, info = match extra_info with
+ | None -> None, info
+ | Some (loc, msg) ->
+ let info = Option.cata (fun l -> Loc.add_loc info l) info loc in
+ msg, info
+ in
+ print_gen ~anomaly ~extra_msg !handle_stack (e,info)
+
(** The standard exception printer *)
-let print ?(info = Exninfo.null) e =
- print_gen (print_anomaly true) !handle_stack e ++ print_backtrace info
+let print ?info e =
+ let info = Option.default Exninfo.(info e) info in
+ print_gen ~anomaly:true (e,info) ++ print_backtrace info
let iprint (e, info) = print ~info e
(** Same as [print], except that the "Please report" part of an anomaly
isn't printed (used in Ltac debugging). *)
-let print_no_report e = print_gen (print_anomaly false) !handle_stack e
+let print_no_report e = print_gen ~anomaly:false (e, Exninfo.info e)
let iprint_no_report (e, info) =
- print_gen (print_anomaly false) !handle_stack e ++ print_backtrace info
+ print_gen ~anomaly:false (e,info) ++ print_backtrace info
(** Predefined handlers **)
diff --git a/lib/cErrors.mli b/lib/cErrors.mli
index 8580622095..100dcd0b22 100644
--- a/lib/cErrors.mli
+++ b/lib/cErrors.mli
@@ -86,3 +86,10 @@ val iprint_no_report : Exninfo.iexn -> Pp.t
Typical example: [Sys.Break], [Assert_failure], [Anomaly] ...
*)
val noncritical : exn -> bool
+
+(** Register a printer for errors carrying additional information on
+ exceptions. This method is fragile and should be considered
+ deprecated *)
+val register_additional_error_info
+ : (Exninfo.info -> (Pp.t option Loc.located) option)
+ -> unit
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' ->
diff --git a/stm/stm.ml b/stm/stm.ml
index ceb62582cd..c5dd367a81 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -116,13 +116,12 @@ let call = get
let call_process_error_once =
let processed : unit Exninfo.t = Exninfo.make () in
- fun (_, info as ei) ->
+ fun (e, info) ->
match Exninfo.get info processed with
- | Some _ -> ei
+ | Some _ -> e, info
| None ->
- let e, info = ExplainErr.process_vernac_interp_error ei in
- let info = Exninfo.add info processed () in
- e, info
+ let info = Exninfo.add info processed () in
+ e, info
end
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 () =
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 =
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:03:37 +0000