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@7909 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 7 insertions, 6 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 4f8df90b5c..cc6dc33e62 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -862,7 +862,7 @@ let compileAutoArg contac = function
 		 then 
 		   tclTHENSEQ [simplest_elim (mkVar id); clear [id]; contac] 
                  else 
-		   tclFAIL 0 ((string_of_id id)^"is not a conjunction"))
+		   tclFAIL 0 (pr_id id ++ str" is not a conjunction"))
 	     ctx) g)
   | UsingTDB ->  
       (tclTHEN  
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index fbd8817892..7aae9f5224 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -138,7 +138,7 @@ let add_rewrite_hint name ort t lcsr =
 
 VERNAC COMMAND EXTEND HintRewrite
   [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident(b) ] ->
-  [ add_rewrite_hint b o (Tacexpr.TacId "") l ]
+  [ add_rewrite_hint b o (Tacexpr.TacId []) l ]
 | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t)
     ":" preident(b) ] ->
   [ add_rewrite_hint b o t l ]
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 517d774d4d..3b5349a4bd 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -91,7 +91,7 @@ let tclLAST_HYP = tclNTH_HYP 1
 
 let tclTRY_sign (tac : constr->tactic) sign gl =
   let rec arec = function
-    | []      -> tclFAIL 0 "no applicable hypothesis"
+    | []      -> tclFAIL 0 (str "no applicable hypothesis")
     | [s]     -> tac (mkVar s) (*added in order to get useful error messages *)
     | (s::sl) -> tclORELSE (tac (mkVar s)) (arec sl) 
   in 
@@ -133,7 +133,7 @@ let simple_clause_list_of cl gls =
 (* OR-branch *)
 let tryClauses tac cl gls = 
   let rec firstrec = function
-    | []      -> tclFAIL 0 "no applicable hypothesis"
+    | []      -> tclFAIL 0 (str "no applicable hypothesis")
     | [cls]   -> tac cls (* added in order to get a useful error message *)
     | cls::tl -> (tclORELSE (tac cls) (firstrec tl))
   in
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 699c0d7801..4b0e39e78f 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -9,6 +9,7 @@
 (*i $Id$ i*)
 
 (*i*)
+open Pp
 open Names
 open Term
 open Sign
@@ -24,7 +25,7 @@ open Tacexpr
 (* Tacticals i.e. functions from tactics to tactics. *)
 
 val tclIDTAC         : tactic
-val tclIDTAC_MESSAGE : string -> tactic
+val tclIDTAC_MESSAGE : std_ppcmds -> tactic
 val tclORELSE        : tactic -> tactic -> tactic
 val tclTHEN          : tactic -> tactic -> tactic
 val tclTHENSEQ       : tactic list -> tactic
@@ -46,7 +47,7 @@ val tclTRY           : tactic -> tactic
 val tclINFO          : tactic -> tactic
 val tclCOMPLETE      : tactic -> tactic
 val tclAT_LEAST_ONCE : tactic -> tactic
-val tclFAIL          : int -> string -> tactic
+val tclFAIL          : int -> std_ppcmds -> tactic
 val tclDO            : int -> tactic -> tactic
 val tclPROGRESS      : tactic -> tactic
 val tclWEAK_PROGRESS : tactic -> tactic