Modifs d'interpretation de patterns

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

5 files changed, 12 insertions, 12 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 067d610fec..7de32f90f0 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -753,7 +753,7 @@ let rec search_gen decomp n db_list local_db extra_sign goal =
   let rec_tacs = 
     List.map 
       (fun ntac -> 
-	 tclTHEN ntac 
+	 tclTHEN ntac
 	   (search_gen decomp (n-1) db_list local_db nil_sign))
       (possible_resolve db_list local_db (pf_concl goal))
   in 
@@ -865,7 +865,7 @@ let compileAutoArg contac = function
                          (clear_one id))
                       contac) 
                  else 
-		   tclFAIL)
+		   tclFAIL 0)
 	      (ids_of_sign ctx) (vals_of_sign ctx)) g)
   | UsingTDB ->  
       (tclTHEN  
diff --git a/tactics/tacentries.ml b/tactics/tacentries.ml
index a91c5f4fc2..4031a11c13 100644
--- a/tactics/tacentries.ml
+++ b/tactics/tacentries.ml
@@ -14,8 +14,8 @@ let v_transitivity  = hide_tactic "Transitivity"  dyn_transitivity
 let v_intro         = hide_tactic "Intro"         dyn_intro
 let v_intro_move    = hide_tactic "IntroMove"     dyn_intro_move
 let v_introsUntil   = hide_tactic "IntrosUntil"   dyn_intros_until
-let v_tclIDTAC      = hide_tactic "Idtac"         dyn_tclIDTAC
-let v_tclFAIL       = hide_tactic "Fail"          dyn_tclFAIL
+(*let v_tclIDTAC      = hide_tactic "Idtac"         dyn_tclIDTAC
+let v_tclFAIL       = hide_tactic "Fail"          dyn_tclFAIL*)
 let v_assumption    = hide_tactic "Assumption"    dyn_assumption
 let v_exact         = hide_tactic "Exact"         dyn_exact
 let v_reduce        = hide_tactic "Reduce"        dyn_reduce
diff --git a/tactics/tacentries.mli b/tactics/tacentries.mli
index bc9e836ab6..6efd48d555 100644
--- a/tactics/tacentries.mli
+++ b/tactics/tacentries.mli
@@ -15,7 +15,7 @@ val v_symmetry      : tactic_arg list -> tactic
 val v_transitivity  : tactic_arg list -> tactic
 val v_intro         : tactic_arg list -> tactic
 val v_introsUntil   : tactic_arg list -> tactic
-val v_tclIDTAC      : tactic_arg list -> tactic
+(*val v_tclIDTAC      : tactic_arg list -> tactic*)
 val v_assumption    : tactic_arg list -> tactic
 val v_exact         : tactic_arg list -> tactic
 val v_reduce        : tactic_arg list -> tactic
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 2bd7df631f..6d9aca72c6 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -45,9 +45,9 @@ let tclWEAK_PROGRESS = Tacmach.tclWEAK_PROGRESS
 let tclMAP tacfun l = 
   List.fold_right (fun x -> (tclTHEN (tacfun x))) l tclIDTAC
 
-let dyn_tclIDTAC = function [] -> tclIDTAC |  _ -> anomaly "tclIDTAC"
+(*let dyn_tclIDTAC = function [] -> tclIDTAC |  _ -> anomaly "tclIDTAC"*)
 
-let dyn_tclFAIL  = function [] -> tclFAIL |  _ -> anomaly "tclFAIL"
+(*let dyn_tclFAIL  = function [] -> tclFAIL |  _ -> anomaly "tclFAIL"*)
 
 (* apply a tactic to the nth element of the signature  *)
 
@@ -61,7 +61,7 @@ let tclLAST_HYP = tclNTH_HYP 1
 
 let tclTRY_sign (tac : constr->tactic) sign gl =
   let rec arec = function
-    | []      -> tclFAIL
+    | []      -> tclFAIL 0
     | [s]     -> tac (VAR(s)) (* added in order to get useful error messages *)
     | (s::sl) -> tclORELSE (tac (VAR(s))) (arec sl) 
   in 
@@ -73,7 +73,7 @@ let tclTRY_HYPS (tac : constr->tactic) gl =
 (* OR-branch *)
 let tryClauses tac = 
   let rec firstrec = function
-    | []      -> tclFAIL
+    | []      -> tclFAIL 0
     | [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 7a0e3f9c51..056ac353f2 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -27,7 +27,7 @@ val tclTRY           : tactic -> tactic
 val tclINFO          : tactic -> tactic
 val tclCOMPLETE      : tactic -> tactic
 val tclAT_LEAST_ONCE : tactic -> tactic
-val tclFAIL          : tactic
+val tclFAIL          : int -> tactic
 val tclDO            : int -> tactic -> tactic
 val tclPROGRESS      : tactic -> tactic
 val tclWEAK_PROGRESS : tactic -> tactic
@@ -37,8 +37,8 @@ val tclLAST_HYP      : (constr -> tactic) -> tactic
 val tclTRY_sign      : (constr -> tactic) -> constr signature -> tactic
 val tclTRY_HYPS      : (constr -> tactic) -> tactic
 
-val dyn_tclIDTAC     : tactic_arg list -> tactic
-val dyn_tclFAIL      : tactic_arg list -> tactic
+(*val dyn_tclIDTAC     : tactic_arg list -> tactic
+val dyn_tclFAIL      : tactic_arg list -> tactic*)
 
 (*s Clause tacticals. *)