diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.mlg | 1 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 16 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 3 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 4 | ||||
| -rw-r--r-- | plugins/ltac/tactic_debug.ml | 17 | ||||
| -rw-r--r-- | plugins/ssr/ssrvernac.mlg | 9 |
7 files changed, 18 insertions, 34 deletions
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' -> |