diff options
| -rw-r--r-- | dev/base_include | 4 | ||||
| -rw-r--r-- | dev/printers.mllib | 2 | ||||
| -rw-r--r-- | ltac/tactic_debug.ml | 7 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 2 | ||||
| -rw-r--r-- | toplevel/explainErr.ml (renamed from toplevel/cerrors.ml) | 0 | ||||
| -rw-r--r-- | toplevel/explainErr.mli (renamed from toplevel/cerrors.mli) | 0 | ||||
| -rw-r--r-- | toplevel/obligations.ml | 4 | ||||
| -rw-r--r-- | toplevel/toplevel.mllib | 2 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
14 files changed, 18 insertions, 17 deletions
diff --git a/dev/base_include b/dev/base_include index 86f34b2ac..b09b6df2d 100644 --- a/dev/base_include +++ b/dev/base_include @@ -66,7 +66,7 @@ open Univ open Inductive open Indtypes open Cooking -open Closure +open CClosure open Reduction open Safe_typing open Declare @@ -170,7 +170,7 @@ open Tacticals open Tactics open Eqschemes -open Cerrors +open ExplainErr open Class open Command open Indschemes diff --git a/dev/printers.mllib b/dev/printers.mllib index a2a7437fb..316549548 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -208,7 +208,7 @@ Dn Btermdn Hints Himsg -Cerrors +ExplainErr Locality Assumptions Vernacinterp diff --git a/ltac/tactic_debug.ml b/ltac/tactic_debug.ml index 362bf3f24..e1c9fed63 100644 --- a/ltac/tactic_debug.ml +++ b/ltac/tactic_debug.ml @@ -36,10 +36,11 @@ type debug_info = (* An exception handler *) let explain_logic_error e = - CErrors.print (fst (Cerrors.process_vernac_interp_error (e, Exninfo.null))) + CErrors.print (fst (ExplainErr.process_vernac_interp_error (e, Exninfo.null))) let explain_logic_error_no_anomaly e = - CErrors.print_no_report (fst (Cerrors.process_vernac_interp_error (e, Exninfo.null))) + CErrors.print_no_report + (fst (ExplainErr.process_vernac_interp_error (e, Exninfo.null))) let msg_tac_debug s = Proofview.NonLogical.print_debug (s++fnl()) let msg_tac_notice s = Proofview.NonLogical.print_notice (s++fnl()) @@ -417,4 +418,4 @@ let get_ltac_trace (_, info) = | None -> None | Some trace -> Some (extract_ltac_trace trace loc) -let () = Cerrors.register_additional_error_info get_ltac_trace +let () = ExplainErr.register_additional_error_info get_ltac_trace diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 215c850b6..b0ffc775b 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -27,7 +27,7 @@ let observe strm = let do_observe_tac s tac g = try let v = tac g in (* msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); *) v with e -> - let e = Cerrors.process_vernac_interp_error e in + let e = ExplainErr.process_vernac_interp_error e in let goal = begin try (Printer.pr_goal g) with _ -> assert false end in msg_debug (str "observation "++ s++str " raised exception " ++ Errors.print e ++ str " on goal " ++ goal ); @@ -76,7 +76,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 (Cerrors.process_vernac_interp_error reraise))); + then print_debug_queue (Some (fst (ExplainErr.process_vernac_interp_error reraise))); iraise reraise let observe_tac_stream s tac g = diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 85897ecee..42e490315 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -195,7 +195,7 @@ END let warning_error names e = - let (e, _) = Cerrors.process_vernac_interp_error (e, Exninfo.null) in + let (e, _) = ExplainErr.process_vernac_interp_error (e, Exninfo.null) in match e with | Building_graph e -> let names = pr_enum Libnames.pr_reference names in diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 6e33af8fb..18817f504 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -225,7 +225,7 @@ let prepare_body ((name,_,args,types,_),_) rt = (fun_args,rt') let process_vernac_interp_error e = - fst (Cerrors.process_vernac_interp_error (e, Exninfo.null)) + fst (ExplainErr.process_vernac_interp_error (e, Exninfo.null)) let warn_funind_cannot_build_inversion = CWarnings.create ~name:"funind-cannot-build-inversion" ~category:"funind" diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index e0c60d6d5..26fc88a60 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -72,7 +72,7 @@ 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 = Cerrors.process_vernac_interp_error 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 )); iraise reraise;; diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 027fe5677..62f307115 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -240,7 +240,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 (Cerrors.process_vernac_interp_error reraise)); + then print_debug_queue true (fst (ExplainErr.process_vernac_interp_error reraise)); iraise reraise let observe_tac s tac g = diff --git a/toplevel/cerrors.ml b/toplevel/explainErr.ml index 17897460c..17897460c 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/explainErr.ml diff --git a/toplevel/cerrors.mli b/toplevel/explainErr.mli index a67c887af..a67c887af 100644 --- a/toplevel/cerrors.mli +++ b/toplevel/explainErr.mli diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 1be5226de..1f1be243e 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -872,7 +872,7 @@ let obligation_terminator name num guard hook auto pf = end with e when CErrors.noncritical e -> let e = CErrors.push e in - pperror (CErrors.iprint (Cerrors.process_vernac_interp_error e)) + pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e)) let obligation_hook prg obl num auto ctx' _ gr = let obls, rem = prg.prg_obligations in @@ -903,7 +903,7 @@ in try ignore (update_obls prg obls (pred rem)) with e when CErrors.noncritical e -> let e = CErrors.push e in - pperror (CErrors.iprint (Cerrors.process_vernac_interp_error e)) + pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e)) in if pred rem > 0 then begin let deps = dependencies obls num in diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index 5aa7d428a..d68922363 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -1,5 +1,5 @@ Himsg -Cerrors +ExplainErr Class Locality Metasyntax diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 3423a8b8c..0559934ec 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -378,4 +378,4 @@ let compile v f = CoqworkmgrApi.giveback 1 let () = Hook.set Stm.process_error_hook - Cerrors.process_vernac_interp_error + ExplainErr.process_vernac_interp_error diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index e4a2ca5a0..f69c4fa18 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -2009,7 +2009,7 @@ let with_fail b f = | e -> let e = CErrors.push e in raise (HasFailed (CErrors.iprint - (Cerrors.process_vernac_interp_error ~allow_uncaught:false ~with_header:false e)))) + (ExplainErr.process_vernac_interp_error ~allow_uncaught:false ~with_header:false e)))) () with e when CErrors.noncritical e -> let (e, _) = CErrors.push e in |