diff options
| author | herbelin | 2010-10-23 09:32:36 +0000 |
|---|---|---|
| committer | herbelin | 2010-10-23 09:32:36 +0000 |
| commit | d77eaf1431ee13066ee5e55074297bbb4b4d4197 (patch) | |
| tree | 17c66653c660a67a7d62d736cad47b835eb6389e | |
| parent | 34c87d7eb06543442bbba295e2e86feff86b192a (diff) | |
Fixing bug #2412 (preprocessing of Ltac Debug errors forgotten in r13431).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13573 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/cerrors.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index a34afda50f..13712ebbed 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -146,10 +146,13 @@ let explain_exn_default = let raise_if_debug e = if !Flags.debug then raise e -let _ = Tactic_debug.explain_logic_error := explain_exn_default +let _ = Tactic_debug.explain_logic_error := + (fun e -> explain_exn_default (process_vernac_interp_error e)) let _ = Tactic_debug.explain_logic_error_no_anomaly := - explain_exn_default_aux (fun () -> mt()) (fun () -> str ".") + (fun e -> + explain_exn_default_aux mt (fun () -> str ".") + (process_vernac_interp_error e)) let explain_exn_function = ref explain_exn_default |