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

7 files changed, 12 insertions, 12 deletions

diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml
index a3e1902c06..e6ce0ad662 100644
--- a/contrib/cc/cctac.ml
+++ b/contrib/cc/cctac.ml
@@ -287,7 +287,7 @@ let cc_tactic additionnal_terms gls=
   let _ = debug Pp.msgnl (Pp.str "Computation completed.") in
   let uf=forest state in
     match sol with
-	None -> tclFAIL 0 "congruence failed" gls  
+	None -> tclFAIL 0 (str "congruence failed") gls  
       | Some reason ->
 	  debug Pp.msgnl (Pp.str "Goal solved, generating proof ...");
 	  match reason with
@@ -318,7 +318,7 @@ let cc_tactic additionnal_terms gls=
 		       end);
 		  Pp.msgnl
 		    (Pp.str "  replacing metavariables by arbitrary terms.");
-		  tclFAIL 0 "Incomplete" gls
+		  tclFAIL 0 (str "Incomplete") gls
 	    | Contradiction dis ->
 		let p=build_proof uf (`Prove (dis.lhs,dis.rhs)) in
 		let ta=term uf dis.lhs and tb=term uf dis.rhs in
diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4
index 0db32a5557..e6f7b03cb2 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 00a2260c6f..9f9a7e68dd 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 0b371966b9..eac842b86a 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 727a03000e..bc4699ea19 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)
 
diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4
index 27c0658d29..bf918ba560 100644
--- a/contrib/funind/tacinv.ml4
+++ b/contrib/funind/tacinv.ml4
@@ -597,7 +597,7 @@ let rec iterintro i =
         let sub = 
          try String.sub hypname 0 (String.length heq_prefix)
          with _ -> "" (* different than [heq_prefix] *) in
-        if sub=heq_prefix then rewriteLR hyp else tclFAIL 0 "Cannot rewrite")
+        if sub=heq_prefix then rewriteLR hyp else tclFAIL 0 (str "Cannot rewrite"))
       )) gl)
 
 
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index 1671c405a1..2e62aa407e 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -247,7 +247,7 @@ let list_rewrite (rev:bool) (eqs: constr list) =
   tclREPEAT
     (List.fold_right
        (fun eq i -> tclORELSE (rewriteLR eq) i)
-       (if rev then (List.rev eqs) else eqs) (tclFAIL 0 ""));;
+       (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));;
 
 let base_leaf (func:global_reference) eqs expr =
 (*  let _ = msgnl (str "entering base_leaf") in *)