Ajout d'un message à FailTac

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3825 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 15 insertions, 13 deletions

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 293a2434aa..61fc3f3b1d 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -347,10 +347,10 @@ let tclIDTAC gls = (goal_goal_list gls, idtac_valid)
 let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s)
 
 (* A special exception for levels for the Fail tactic *)
-exception FailError of int
+exception FailError of int * string
 
 (* The Fail tactic *)
-let tclFAIL lvl g = raise (FailError lvl)
+let tclFAIL lvl s g = raise (FailError (lvl,s))
 
 let start_tac gls =
   let (sigr,g) = unpackage gls in
@@ -508,10 +508,10 @@ let tclORELSE0 t1 t2 g =
     t1 g
   with
   | e when catchable_exception e -> t2 g
-  | FailError 0 | Stdpp.Exc_located(_, FailError 0) -> t2 g
-  | FailError lvl -> raise (FailError (lvl - 1))
-  | Stdpp.Exc_located (s,FailError lvl) ->
-      raise (Stdpp.Exc_located (s,FailError (lvl - 1)))
+  | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_)) -> t2 g
+  | FailError (lvl,s) -> raise (FailError (lvl - 1, s))
+  | Stdpp.Exc_located (s,FailError (lvl,s')) ->
+      raise (Stdpp.Exc_located (s,FailError (lvl - 1, s')))
 
 (* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress, 
    then applies t2 *)
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index c0d047edbf..6ea71c4db2 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -119,7 +119,7 @@ val tclTHENLASTn    : tactic -> tactic array -> tactic
 val tclTHENFIRSTn   : tactic -> tactic array -> tactic
 
 (* A special exception for levels for the Fail tactic *)
-exception FailError of int
+exception FailError of int * string
 
 val tclORELSE        : tactic -> tactic -> tactic
 val tclREPEAT        : tactic -> tactic
@@ -130,7 +130,7 @@ val tclTRY           : tactic -> tactic
 val tclTHENTRY       : tactic -> tactic -> tactic
 val tclCOMPLETE      : tactic -> tactic
 val tclAT_LEAST_ONCE : tactic -> tactic
-val tclFAIL          : int -> tactic
+val tclFAIL          : int -> string -> tactic
 val tclDO            : int -> tactic -> tactic
 val tclPROGRESS      : tactic -> tactic
 val tclWEAK_PROGRESS : tactic -> tactic
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 1c6d7a6f60..146d4bd293 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -184,7 +184,7 @@ and ('constr,'cst,'ind,'id) gen_tactic_expr =
   | TacProgress of ('constr,'cst,'ind,'id) gen_tactic_expr
   | TacAbstract of ('constr,'cst,'ind,'id) gen_tactic_expr * identifier option
   | TacId
-  | TacFail of int
+  | TacFail of int * string
   | TacInfo of ('constr,'cst,'ind,'id) gen_tactic_expr
 
   | TacLetRecIn of (identifier located * ('constr,'cst,'ind,'id) gen_tactic_fun_ast) list * ('constr,'cst,'ind,'id) gen_tactic_expr
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())
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index 8c5dc9d03c..82f01f461b 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -54,7 +54,7 @@ val db_hyp_pattern_failure :
 val db_matching_failure : debug_info -> unit
 
 (* Prints an evaluation failure message for a rule *)
-val db_eval_failure : debug_info -> unit
+val db_eval_failure : debug_info -> string -> unit
 
 (* An exception handler *)
 val explain_logic_error: (exn -> Pp.std_ppcmds) ref