diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-27 18:15:07 +0200 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2016-07-03 12:16:24 +0200 |
| commit | 3ce70f21a18cc19e720e8ac54b93652527881942 (patch) | |
| tree | c07c40d207b60b9c31fc148fc720b3890deb7f56 /ltac | |
| parent | cf95f2a791c263c7aaa3b488d1b09eaafc29be2b (diff) | |
rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cErrors.ml)
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/tactic_debug.ml | 7 |
1 files changed, 4 insertions, 3 deletions
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 |