diff options
Diffstat (limited to 'toplevel/cerrors.ml')
| -rw-r--r-- | toplevel/cerrors.ml | 31 |
1 files changed, 16 insertions, 15 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 8c98c813a..03c9afbf7 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -53,12 +53,12 @@ let _ = Errors.register_handler explain_exn_default (** Pre-explain a vernac interpretation error *) -let wrap_vernac_error exn strm = +let wrap_vernac_error (exn, info) strm = let header = Pp.tag (Pp.Tag.inj Ppstyle.error_tag Ppstyle.tag) (str "Error:") in let e = EvaluatedError (hov 0 (header ++ spc () ++ strm), None) in - Exninfo.copy exn e + (e, info) -let process_vernac_interp_error exn = match exn with +let process_vernac_interp_error exn = match fst exn with | Univ.UniverseInconsistency i -> let msg = if !Constrextern.print_universes then @@ -99,29 +99,30 @@ let process_vernac_interp_error exn = match exn with if Int.equal i 0 then str "." else str " (level " ++ int i ++ str").") | AlreadyDeclared msg -> wrap_vernac_error exn (msg ++ str ".") - | exc -> - exc + | _ -> + exn let rec strip_wrapping_exceptions = function - | Logic_monad.TacticFailure e as src -> - let e = Backtrace.app_backtrace ~src ~dst:e in + | Logic_monad.TacticFailure e -> strip_wrapping_exceptions e | exc -> exc -let process_vernac_interp_error exc = +let process_vernac_interp_error (exc, info) = let exc = strip_wrapping_exceptions exc in - let e = process_vernac_interp_error exc in - let ltac_trace = Exninfo.get exc Proof_type.ltac_trace_info in - let loc = Option.default Loc.ghost (Loc.get_loc e) in + let e = process_vernac_interp_error (exc, info) in + let ltac_trace = Exninfo.get info Proof_type.ltac_trace_info in + let loc = Option.default Loc.ghost (Loc.get_loc info) in match ltac_trace with | None -> e | Some trace -> + let (e, info) = e in match Himsg.extract_ltac_trace trace loc with - | None, loc -> Loc.add_loc e loc - | Some msg, loc -> Loc.add_loc (EvaluatedError (msg, Some e)) loc + | None, loc -> (e, Loc.add_loc info loc) + | Some msg, loc -> + (EvaluatedError (msg, Some e), Loc.add_loc info loc) let _ = Tactic_debug.explain_logic_error := - (fun e -> Errors.print (process_vernac_interp_error e)) + (fun e -> Errors.print (fst (process_vernac_interp_error (e, Exninfo.null)))) let _ = Tactic_debug.explain_logic_error_no_anomaly := - (fun e -> Errors.print_no_report (process_vernac_interp_error e)) + (fun e -> Errors.print_no_report (fst (process_vernac_interp_error (e, Exninfo.null)))) |