Messages de idtac et fail peuvent maintenant être des listes de string, int et variables ltac

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

4 files changed, 8 insertions, 12 deletions

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 1bc19c9105..dd719e48e4 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -335,17 +335,13 @@ let tclIDTAC gls = (goal_goal_list gls, idtac_valid)
 
 (* the message printing identity tactic *)
 let tclIDTAC_MESSAGE s gls = 
-  if s = "" then tclIDTAC gls
-  else 
-    begin
-      msgnl (str ("Idtac says : "^s)); tclIDTAC gls
-    end
+  msg (hov 0 s); tclIDTAC gls
 
 (* General failure tactic *)
 let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s)
 
 (* A special exception for levels for the Fail tactic *)
-exception FailError of int * string
+exception FailError of int * std_ppcmds
 
 (* The Fail tactic *)
 let tclFAIL lvl s g = raise (FailError (lvl,s))
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index b21485e456..41b312e5db 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -66,7 +66,7 @@ val frontier_mapi :
 
 (* [tclIDTAC] is the identity tactic without message printing*)
 val tclIDTAC          : tactic
-val tclIDTAC_MESSAGE  : string -> tactic
+val tclIDTAC_MESSAGE  : Pp.std_ppcmds -> tactic
 
 (* [tclEVARS sigma] changes the current evar map *)
 val tclEVARS : evar_map -> tactic
@@ -123,7 +123,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 * string
+exception FailError of int * Pp.std_ppcmds
 
 val tclORELSE        : tactic -> tactic -> tactic
 val tclREPEAT        : tactic -> tactic
@@ -134,7 +134,7 @@ val tclTRY           : tactic -> tactic
 val tclTHENTRY       : tactic -> tactic -> tactic
 val tclCOMPLETE      : tactic -> tactic
 val tclAT_LEAST_ONCE : tactic -> tactic
-val tclFAIL          : int -> string -> tactic
+val tclFAIL          : int -> Pp.std_ppcmds -> tactic
 val tclDO            : int -> tactic -> tactic
 val tclPROGRESS      : tactic -> tactic
 val tclWEAK_PROGRESS : tactic -> tactic
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 5d2cbd57b8..43807872dc 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -162,10 +162,10 @@ let db_matching_failure debug =
 (* Prints an evaluation failure message for a rule *)
 let db_eval_failure debug s =
   if debug <> DebugOff & !skip = 0 then
-    let s = if s="" then "no message" else "message \""^s^"\"" in
+    let s = str "message \"" ++ s ++ str "\"" in
     msgnl 
       (str "This rule has failed due to \"Fail\" tactic (" ++
-       str s ++ str ", level 0)!" ++ fnl() ++ str "Let us try the next one...")
+       s ++ str ", level 0)!" ++ fnl() ++ str "Let us try the next one...")
 
 (* Prints a logic failure message for a rule *)
 let db_logic_failure debug err =
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index 27536dfa93..a649656052 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -61,7 +61,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 -> string -> unit
+val db_eval_failure : debug_info -> Pp.std_ppcmds -> unit
 
 (* An exception handler *)
 val explain_logic_error: (exn -> Pp.std_ppcmds) ref