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, 8 insertions, 8 deletions

diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4
index 0db32a555..e6f7b03cb 100644
--- a/contrib/first-order/g_ground.ml4
+++ b/contrib/first-order/g_ground.ml4
@@ -41,7 +41,7 @@ let _=
       
 let default_solver=(Tacinterp.interp <:tactic<auto with *>>)
     
-let fail_solver=tclFAIL 0 "GTauto failed"
+let fail_solver=tclFAIL 0 (Pp.str "GTauto failed")
 		      
 type external_env=
     Ids of global_reference list
diff --git a/contrib/first-order/ground.ml b/contrib/first-order/ground.ml
index 00a2260c6..9f9a7e68d 100644
--- a/contrib/first-order/ground.ml
+++ b/contrib/first-order/ground.ml
@@ -78,7 +78,7 @@ let ground_tac solver startseq gl=
 		      | Rforall->
 			  let backtrack1=
 			    if !qflag then 
-			      tclFAIL 0 "reversible in 1st order mode"
+			      tclFAIL 0 (Pp.str "reversible in 1st order mode")
 			    else
 			      backtrack in
 			    forall_tac backtrack continue (re_add seq1)
diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml
index 0b371966b..eac842b86 100644
--- a/contrib/first-order/instances.ml
+++ b/contrib/first-order/instances.ml
@@ -138,7 +138,7 @@ let left_instance_tac (inst,id) continue seq=
   match inst with
       Phantom dom->
 	if lookup (id,None) seq then 
-	  tclFAIL 0 "already done"
+	  tclFAIL 0 (Pp.str "already done")
 	else
 	  tclTHENS (cut dom) 
 	    [tclTHENLIST
@@ -152,7 +152,7 @@ let left_instance_tac (inst,id) continue seq=
 	    tclTRY assumption]
     | Real((m,t) as c,_)->
 	if lookup (id,Some c) seq then 
-	  tclFAIL 0 "already done" 
+	  tclFAIL 0 (Pp.str "already done")
 	else 
 	  let special_generalize=
 	    if m>0 then 
@@ -186,7 +186,7 @@ let right_instance_tac inst continue seq=
 	(tclTHEN (split (Rawterm.ImplicitBindings [t]))
 	   (tclSOLVE [wrap 0 true continue (deepen seq)]))
     | Real ((m,t),_) ->
-	tclFAIL 0 "not implemented ... yet"
+	tclFAIL 0 (Pp.str "not implemented ... yet")
 
 let instance_tac inst=
   if (snd inst)==dummy_id then 
diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
index 727a03000..bc4699ea1 100644
--- a/contrib/first-order/rules.ml
+++ b/contrib/first-order/rules.ml
@@ -58,7 +58,7 @@ let clear_global=function
 
 let axiom_tac t seq=
   try exact_no_check (constr_of_global (find_left t seq)) 
-  with Not_found->tclFAIL 0 "No axiom link" 
+  with Not_found->tclFAIL 0 (Pp.str "No axiom link")
 
 let ll_atom_tac a backtrack id continue seq= 
   tclIFTHENELSE
@@ -68,7 +68,7 @@ let ll_atom_tac a backtrack id continue seq=
 			   [|constr_of_global (find_left a seq)|])];
 	 clear_global id;
 	 intro]
-    with Not_found->tclFAIL 0 "No link") 
+    with Not_found->tclFAIL 0 (Pp.str "No link"))
     (wrap 1 false continue seq) backtrack 
 
 (* right connectives rules *)
@@ -168,7 +168,7 @@ let forall_tac backtrack continue seq=
 	  (tclTHEN introf (tclCOMPLETE (wrap 0 true continue seq)))
 	  backtrack))
     (if !qflag then 
-       tclFAIL 0 "reversible in 1st order mode"
+       tclFAIL 0 (Pp.str "reversible in 1st order mode")
      else
        backtrack)