From d77eaf1431ee13066ee5e55074297bbb4b4d4197 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 23 Oct 2010 09:32:36 +0000
Subject: 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
---
 toplevel/cerrors.ml | 7 +++++--
 1 file 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
 
-- 
cgit v1.2.3