From f14b6f1a17652566f0cbc00ce81421ba0684dad5 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 27 Jun 2016 11:03:43 +0200 Subject: errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a --- ltac/tactic_debug.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'ltac/tactic_debug.ml') diff --git a/ltac/tactic_debug.ml b/ltac/tactic_debug.ml index 73d04b810d..362bf3f24a 100644 --- a/ltac/tactic_debug.ml +++ b/ltac/tactic_debug.ml @@ -36,10 +36,10 @@ type debug_info = (* An exception handler *) let explain_logic_error e = - Errors.print (fst (Cerrors.process_vernac_interp_error (e, Exninfo.null))) + CErrors.print (fst (Cerrors.process_vernac_interp_error (e, Exninfo.null))) let explain_logic_error_no_anomaly e = - Errors.print_no_report (fst (Cerrors.process_vernac_interp_error (e, Exninfo.null))) + CErrors.print_no_report (fst (Cerrors.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()) -- cgit v1.2.3 From 3ce70f21a18cc19e720e8ac54b93652527881942 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 27 Jun 2016 18:15:07 +0200 Subject: rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cErrors.ml) --- ltac/tactic_debug.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'ltac/tactic_debug.ml') diff --git a/ltac/tactic_debug.ml b/ltac/tactic_debug.ml index 362bf3f24a..e1c9fed637 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 -- cgit v1.2.3