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, 11 insertions, 10 deletions

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index e397cd0cfe..e44b66bd4a 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -574,10 +574,10 @@ let res_tac c a hyp =
   let fin = match hyp with
     | None -> Auto.full_trivial
     | Some h -> 
-	tclORELSE (tclTHEN (tclTRY (apply h)) (tclFAIL 0)) 
-	(tclORELSE (tclTHEN (tclTRY (tclTHEN (apply (mkApp ((Lazy.force coq_seq_sym), [|sa.set_a; sa.set_aeq; sa.set_th|]))) (apply h))) (tclFAIL 0))
+	tclORELSE (tclTHEN (tclTRY (apply h)) (tclFAIL 0 "")) 
+	(tclORELSE (tclTHEN (tclTRY (tclTHEN (apply (mkApp ((Lazy.force coq_seq_sym), [|sa.set_a; sa.set_aeq; sa.set_th|]))) (apply h))) (tclFAIL 0 ""))
 	   Auto.full_trivial) in
-    tclORELSE (tclTHEN (tclTRY (apply (mkApp ((Lazy.force coq_seq_refl), [|sa.set_a; sa.set_aeq; sa.set_th;c|])))) (tclFAIL 0))
+    tclORELSE (tclTHEN (tclTRY (apply (mkApp ((Lazy.force coq_seq_refl), [|sa.set_a; sa.set_aeq; sa.set_th;c|])))) (tclFAIL 0 ""))
       (tclORELSE assumption
 	 (tclORELSE (tclTHEN (tclTRY (apply (mkApp ((Lazy.force coq_seq_sym), [|sa.set_a; sa.set_aeq; sa.set_th|])))) assumption)
 	    fin))
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 9d63f33ef4..d3c57c45b6 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -23,7 +23,7 @@ open Topconstr
 
 (* Values for interpretation *)
 type value =
-  | VTactic of tactic  (* For mixed ML/Ltac tactics (e.g. Tauto) *)
+  | VTactic of Util.loc * tactic  (* For mixed ML/Ltac tactics (e.g. Tauto) *)
   | VRTactic of (goal list sigma * validation)
   | VFun of (identifier * value) list * identifier option list *raw_tactic_expr
   | VVoid
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 08004e9718..f6be87bcf6 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -85,7 +85,7 @@ let tclLAST_HYP = tclNTH_HYP 1
 
 let tclTRY_sign (tac : constr->tactic) sign gl =
   let rec arec = function
-    | []      -> tclFAIL 0
+    | []      -> tclFAIL 0 "no applicable hypothesis"
     | [s]     -> tac (mkVar s) (*added in order to get useful error messages *)
     | (s::sl) -> tclORELSE (tac (mkVar s)) (arec sl) 
   in 
@@ -97,7 +97,7 @@ let tclTRY_HYPS (tac : constr->tactic) gl =
 (* OR-branch *)
 let tryClauses tac = 
   let rec firstrec = function
-    | []      -> tclFAIL 0
+    | []      -> tclFAIL 0 "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 0557be8829..a32eaf54fd 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -44,7 +44,7 @@ val tclTRY           : tactic -> tactic
 val tclINFO          : 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/tactics/tauto.ml4 b/tactics/tauto.ml4
index 36ee7e18a6..bf9059c757 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -144,7 +144,8 @@ let reduction_not_iff=interp
 	   Progress Unfold Coq.Init.Logic.not Coq.Init.Logic.iff in H)>>
 
 
-let t_reduction_not_iff = Tacexpr.TacArg (valueIn (VTactic reduction_not_iff))
+let t_reduction_not_iff =
+  Tacexpr.TacArg (valueIn (VTactic (dummy_loc,reduction_not_iff)))
 
 let intuition_gen tac =
   interp (tacticIn (tauto_intuit t_reduction_not_iff tac))
@@ -166,9 +167,9 @@ let q_elim tac=
       Generalize (H x);Clear H;$tac>>
 
 let rec lfo n gl=
-  if n=0 then (tclFAIL 0 gl) else
+  if n=0 then (tclFAIL 0 "LinearIntuition failed" gl) else
     let p=if n<0 then n else (n-1) in
-    let lfo_rec=q_elim (Tacexpr.TacArg (valueIn (VTactic (lfo p)))) in
+    let lfo_rec=q_elim (Tacexpr.TacArg (valueIn (VTactic(dummy_loc,lfo p)))) in
       intuition_gen lfo_rec gl
 
 let lfo_wrap n gl=