From 00608fac2d8e217232d5f2ddd28a43971bf259b7 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 31 Mar 2003 21:18:53 +0000
Subject: Ajout d'un message à FailTac

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3825 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/tactic_debug.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'proofs/tactic_debug.ml')

diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 592f3a2eab..9c0b77f581 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -159,10 +159,12 @@ let db_matching_failure debug =
            str "Let us try the next one...")
 
 (* Prints an evaluation failure message for a rule *)
-let db_eval_failure debug =
+let db_eval_failure debug s =
   if debug = DebugOn then
-    msgnl (str "This rule has failed due to \"Fail\" tactic (level 0)!" ++
-           fnl() ++ str "Let us try the next one...")
+    let s = if s="" then "no message" else "message \""^s^"\"" in
+    msgnl 
+      (str "This rule has failed due to \"Fail\" tactic (" ++
+       str s ++ str ", level 0)!" ++ fnl() ++ str "Let us try the next one...")
 
 (* An exception handler *)
 let explain_logic_error = ref (fun e -> mt())
-- 
cgit v1.2.3