Modifs d'interpretation de patterns

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

13 files changed, 153 insertions, 94 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 4e658787d0..68a75ee32d 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -462,6 +462,7 @@ let unsafe_fmachine tycon nocheck isevars metamap env lvar lmeta constr =
   reset_problems ();
   pretype tycon env isevars lvar lmeta constr
 
+
 let unsafe_fmachine_type valcon nocheck isevars metamap env lvar lmeta constr =
   trad_metamap := metamap;
   trad_nocheck := nocheck;
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 72cd94c1dc..60647a946c 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -44,7 +44,10 @@ let rec type_of env cstr=
           (try strip_outer_cast (List.assoc n metamap)
            with Not_found -> anomaly "type_of: this is not a well-typed term")
     | IsRel n -> lift n (body_of_type (snd (lookup_rel n env)))
-    | IsVar id -> body_of_type (snd (lookup_var id env))
+    | IsVar id ->
+      (try body_of_type (snd (lookup_var id env))
+       with Not_found ->
+         anomaly ("type_of: variable "^(string_of_id id)^" unbound"))
     | IsAbst _ -> error "No more Abst" (*type_of env (abst_value cstr)*)
     | IsConst c -> body_of_type (type_of_constant env sigma c)
     | IsEvar _ -> type_of_existential env sigma cstr
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 915431d597..1a16f77448 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -323,7 +323,13 @@ let tclIDTAC gls = (goal_goal_list gls, idtac_valid);;
 
 (* General failure tactic *)
 let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" [< 'sTR s>];;
-let tclFAIL = tclFAIL_s "Failtac always fails.";;
+
+(* A special exception for levels for the Fail tactic *)
+exception FailError of int
+
+(* The Fail tactic *)
+let tclFAIL lvl g = raise (FailError lvl)
+
 let start_tac gls =
   let (sigr,g) = unpackage gls in
   (sigr,[g],idtac_valid)
@@ -449,8 +455,13 @@ let tclNOTSAMEGOAL (tac : tactic) goal =
 let tclORELSE0 t1 t2 g =
   try 
     t1 g
-  with e when catchable_exception e -> 
-    t2 g
+  with
+  | e when catchable_exception e -> t2 g
+  | FailError lvl ->
+    if lvl = 0 then
+      t2 g
+    else
+      raise (FailError (lvl - 1))
 
 (* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress, 
    then applies t2 *)
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index d2d2794f0c..5c2b24d7fc 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -73,6 +73,9 @@ val tclTHENS         : tactic -> tactic list -> tactic
   subgoals is strictly less than [n] *)
 val tclTHENSI        : tactic -> tactic list -> tactic
 
+(* A special exception for levels for the Fail tactic *)
+exception FailError of int
+
 val tclORELSE        : tactic -> tactic -> tactic
 val tclREPEAT        : tactic -> tactic
 val tclFIRST         : tactic list -> tactic
@@ -81,7 +84,7 @@ val tclTRY           : tactic -> tactic
 val tclTHENTRY       : tactic -> 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
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index c01a547d6a..c95424fb18 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -45,6 +45,30 @@ let constr_of_Constr = function
   | Constr c -> c
   | _ -> anomalylabstrm "constr_of_Constr" [<'sTR "Not a CONSTR tactic_arg">]
 
+(* Transforms a type_judgment signature into a (string * constr) list *)
+let make_hyps hyps =
+  let lid = List.map string_of_id (ids_of_sign hyps)
+  and lhyp = List.map body_of_type (vals_of_sign hyps) in
+    List.rev (List.combine lid lhyp)
+
+(* Extracted the constr list from lfun *)
+let rec constr_list goalopt = function
+  | (str,VArg(Constr c))::tl -> (id_of_string str,c)::(constr_list goalopt tl)
+  | (str,VArg(Identifier id))::tl ->
+    (try
+       (id_of_string str,Declare.global_reference CCI id)::(constr_list
+         goalopt tl)
+     with | Not_found ->
+       (match goalopt with
+       | None -> constr_list goalopt tl
+       | Some goal ->
+         if List.mem_assoc (string_of_id id) (make_hyps (pf_hyps goal)) then
+           (id_of_string str,VAR id)::(constr_list goalopt tl)
+         else
+           constr_list goalopt tl))
+  | _::tl -> constr_list goalopt tl
+  | [] -> []
+
 (* Signature for interpretation: val_interp and interpretation functions *)
 type interp_sign =
   evar_declarations * Environ.env * (string * value) list *
@@ -186,54 +210,61 @@ let ast_of_command = function
       "Not a COMMAND ast node: "; print_ast ast>])
 
 (* Reads the hypotheses of a Match Context rule *)
-let rec read_match_context_hyps evc env=function
+let rec read_match_context_hyps evc env lfun = function
   | Node(_,"MATCHCONTEXTHYPS",[pc])::tl ->
-    (NoHypId (snd (interp_constrpattern evc env (ast_of_command
-      pc))))::(read_match_context_hyps evc env tl)
+    (NoHypId (snd (interp_constrpattern_gen evc env lfun (ast_of_command
+      pc))))::(read_match_context_hyps evc env lfun tl)
   | Node(_,"MATCHCONTEXTHYPS",[Nvar(_,s);pc])::tl ->
-    (Hyp (s,snd (interp_constrpattern evc env (ast_of_command
-      pc))))::(read_match_context_hyps evc env tl)
+    (Hyp (s,snd (interp_constrpattern_gen evc env lfun (ast_of_command
+      pc))))::(read_match_context_hyps evc env lfun tl)
   | ast::tl ->
     anomaly_loc (Ast.loc ast, "Tacinterp.read_match_context_hyp",[<'sTR
       "Not a MATCHCONTEXTHYP ast node: "; print_ast ast>])
   | [] -> []
 
 (* Reads the rules of a Match Context *)
-let rec read_match_context_rule evc env = function
+let rec read_match_context_rule evc env lfun = function
   | Node(_,"MATCHCONTEXTRULE",[tc])::tl ->
-    (All tc)::(read_match_context_rule evc env tl)
+    (All tc)::(read_match_context_rule evc env lfun tl)
   | Node(_,"MATCHCONTEXTRULE",l)::tl ->
     let rl=List.rev l in
-      (Pat (read_match_context_hyps evc env (List.tl (List.tl rl)),snd
-        (interp_constrpattern evc env (ast_of_command (List.nth rl
-        1))),List.hd rl))::(read_match_context_rule evc env tl)
+      (Pat (read_match_context_hyps evc env lfun (List.tl (List.tl rl)),snd
+        (interp_constrpattern_gen evc env lfun (ast_of_command (List.nth rl
+        1))),List.hd rl))::(read_match_context_rule evc env lfun tl)
   | ast::tl ->
     anomaly_loc (Ast.loc ast, "Tacinterp.read_match_context_rule",[<'sTR
       "Not a MATCHCONTEXTRULE ast node: "; print_ast ast>])
   | [] -> []
 
 (* Reads the rules of a Match *)
-let rec read_match_rule evc env = function
+let rec read_match_rule evc env lfun = function
   | Node(_,"MATCHRULE",[te])::tl ->
-    (All te)::(read_match_rule evc env tl)
+    (All te)::(read_match_rule evc env lfun tl)
   | Node(_,"MATCHRULE",[com;te])::tl ->
-    (Pat ([],snd (interp_constrpattern evc env (ast_of_command com)),te)) ::
-      (read_match_rule evc env tl)
+    (Pat ([],snd (interp_constrpattern_gen evc env lfun
+      (ast_of_command com)),te))::(read_match_rule evc env lfun tl)
   | ast::tl ->
     anomaly_loc (Ast.loc ast, "Tacinterp.read_match_context_rule",[<'sTR
       "Not a MATCHRULE ast node: "; print_ast ast>])
   | [] -> []
 
-(* Transforms a type_judgment signature into a (string * constr) list *)
-let make_hyps hyps =
-  let lid = List.map string_of_id (ids_of_sign hyps)
-  and lhyp = List.map body_of_type (vals_of_sign hyps) in
-    List.combine lid lhyp
-
 (* For Match Context and Match *)
 exception No_match
 exception Not_coherent_metas
 
+(* Evaluation with FailError catching *)
+let eval_with_fail interp ast goal =
+  try 
+    (match interp ast with
+    | VTactic tac -> VRTactic (tac goal)
+    | VFTactic (largs,f) -> VRTactic (f largs goal)
+    | a -> a)
+  with | FailError lvl ->
+    if lvl = 0 then
+      raise No_match
+    else
+      raise (FailError (lvl - 1))
+
 (* Verifies if the matched list is coherent with respect to lcm *)
 let rec verify_metas_coherence lcm = function
   | (num,csr)::tl ->
@@ -308,7 +339,8 @@ let rec val_interp (evc,env,lfun,lmatch,goalopt) ast =
     | Node(_,"MATCH",lmr) ->
       match_interp evc env lfun lmatch goalopt ast lmr
     | Node(_,"IDTAC",[]) -> VTactic tclIDTAC
-    | Node(_,"FAIL",[]) -> VTactic tclFAIL
+    | Node(_,"FAIL",[]) -> VTactic (tclFAIL 0)
+    | Node(_,"FAIL",[n]) -> VTactic (tclFAIL (num_of_ast n))
     | Node(_,"TACTICLIST",l) ->
       VTactic (interp_semi_list tclIDTAC lfun lmatch l)
     | Node(_,"DO",[n;tac]) ->
@@ -333,14 +365,10 @@ let rec val_interp (evc,env,lfun,lmatch,goalopt) ast =
       VFTactic ([],(interp_atomic loc opn))
     | Node(_,"VOID",[]) -> VVoid
     | Nvar(_,s) ->
-      (try
-         (unrec (List.assoc s (List.rev lfun)))
-       with
-           Not_found ->
-             (try
-                (lookup s)
-              with
-                  Not_found -> VArg (Identifier (id_of_string s))))
+      (try (unrec (List.assoc s (List.rev lfun)))
+       with | Not_found ->
+         (try (lookup s)
+          with | Not_found -> VArg (Identifier (id_of_string s))))
     | Str(_,s) -> VArg (Quoted_string s)
     | Num(_,n) -> VArg (Integer n)
     | Node(_,"COMMAND",[c]) -> com_interp (evc,env,lfun,lmatch,goalopt) c
@@ -434,31 +462,33 @@ and let_interp evc env lfun lmatch goalopt ast = function
 
 (* Interprets the Match Context expressions *)
 and match_context_interp evc env lfun lmatch goalopt ast lmr =
-  let rec apply_match_context evc env lfun lmatch goalopt = function
-    | (All t)::tl -> val_interp (evc,env,lfun,lmatch,goalopt) t
+  let goal =
+    (match goalopt with
+    | None ->
+      errorlabstrm "Tacinterp.apply_match_context" [< 'sTR
+        "No goal available" >]
+    | Some g -> g) in
+  let rec apply_match_context evc env lfun lmatch goal = function
+    | (All t)::tl ->
+      (try eval_with_fail (val_interp (evc,env,lfun,lmatch,Some goal)) t goal
+       with No_match -> apply_match_context evc env lfun lmatch goal tl)
     | (Pat (mhyps,mgoal,mt))::tl ->
-      (match goalopt with
-         | None ->
-           errorlabstrm "Tacinterp.apply_match_context" [< 'sTR
-             "No goal available" >]
-         | Some g ->
-           let hyps = make_hyps (pf_hyps g)
-           and concl = pf_concl g in
-             try
-               (let lgoal = apply_matching mgoal concl in
-                  if mhyps = [] then
-                    val_interp (evc,env,lfun,lgoal@lmatch,goalopt) mt
-                  else
-                    apply_hyps_context evc env lfun lmatch g mt lgoal mhyps
-                      hyps)
-             with
-                 No_match ->
-                   apply_match_context evc env lfun lmatch goalopt tl)
+      let hyps = make_hyps (pf_hyps goal)
+      and concl = pf_concl goal in
+      (try
+         (let lgoal = apply_matching mgoal concl in
+          if mhyps = [] then
+            eval_with_fail (val_interp (evc,env,lfun,lgoal@lmatch,Some goal))
+              mt goal
+          else
+            apply_hyps_context evc env lfun lmatch goal mt lgoal mhyps hyps)
+       with
+       | No_match -> apply_match_context evc env lfun lmatch goal tl)
     | _ ->
       errorlabstrm "Tacinterp.apply_match_context" [<'sTR
         "No matching clauses for Match Context">] in
-  apply_match_context evc env lfun lmatch goalopt (read_match_context_rule evc
-    env lmr)
+  apply_match_context evc env lfun lmatch goal (read_match_context_rule evc env
+    (constr_list goalopt lfun) lmr)
 
 (* Tries to match the hypotheses in a Match Context *)
 and apply_hyps_context evc env lfun_glob lmatch_glob goal mt lgmatch mhyps
@@ -480,9 +510,15 @@ and apply_hyps_context evc env lfun_glob lmatch_glob goal mt lgmatch mhyps
                  apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt
                    (lfun@lid) (lmatch@lm) newmhyps (hyps_acc@tl) [])
           with
-              No_match | _ ->
-                apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt
-                  lfun lmatch mhyps tl (hyps_acc@[hd]))
+         | FailError lvl ->
+                if lvl > 0 then
+                  raise (FailError (lvl - 1))
+                else
+                  apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt
+                    lfun lmatch mhyps tl (hyps_acc@[hd])
+         | _ ->
+           apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt lfun
+             lmatch mhyps tl (hyps_acc@[hd]))
       | [] -> raise No_match in
   apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt [] lgmatch mhyps
     hyps []
@@ -503,7 +539,7 @@ and match_interp evc env lfun lmatch goalopt ast lmr =
         "No matching clauses for Match">] in
   let csr = constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt)
     (List.hd lmr)))
-  and ilr = read_match_rule evc env (List.tl lmr) in
+  and ilr = read_match_rule evc env (constr_list goalopt lfun) (List.tl lmr) in
   apply_match evc env lfun lmatch goalopt csr ilr
 
 (* Interprets tactic expressions *)
@@ -552,32 +588,29 @@ and com_interp (evc,env,lfun,lmatch,goalopt) = function
      let redexp = unredexp (unvarg (val_interp (evc,env,lfun,lmatch,goalopt)
        rtc)) in
      VArg (Constr ((reduction_of_redexp redexp) env evc (interp_constr1 evc env
-       (make_subs_list lfun) lmatch c)))
-  | c -> 
-      try
-	VArg (Constr (interp_constr1 evc env (make_subs_list lfun) lmatch c))
-      with e when Logic.catchable_exception e ->
-	VArg (Command c)
+       (constr_list goalopt lfun) lmatch c)))
+  | c ->
+    try
+      VArg (Constr (interp_constr1 evc env (constr_list goalopt lfun) lmatch
+        c))
+    with e when Logic.catchable_exception e -> VArg (Command c)
 
 (* Interprets a CASTEDCOMMAND expression *)
 and cast_com_interp (evc,env,lfun,lmatch,goalopt) com = match goalopt with
   | Some gl ->
       (match com with
          | Node(_,"EVAL",[c;rtc]) ->
-             let redexp = 
-	       unredexp (unvarg (val_interp
-				   (evc,env,lfun,lmatch,goalopt) rtc)) 
-	     in
+             let redexp = unredexp (unvarg (val_interp
+              (evc,env,lfun,lmatch,goalopt) rtc)) in
              VArg (Constr ((reduction_of_redexp redexp) env evc
-			     (interp_casted_constr1 evc env 
-				(make_subs_list lfun) lmatch c (pf_concl gl))))
-         | c ->
-	     try
-               VArg (Constr (interp_casted_constr1 evc env 
-			       (make_subs_list lfun) lmatch c (pf_concl gl)))
-	     with e when Logic.catchable_exception e ->
-	       VArg (Command c))
-  | None ->
+               (interp_casted_constr1 evc env (constr_list goalopt lfun) lmatch
+               c (pf_concl gl))))
+          | c ->
+            try
+              VArg (Constr (interp_casted_constr1 evc env (constr_list goalopt
+                lfun) lmatch c (pf_concl gl)))
+            with e when Logic.catchable_exception e -> VArg (Command c))
+    | None ->
       errorlabstrm "val_interp" [<'sTR "Cannot cast a constr without goal">]
 
 and cvt_pattern (evc,env,lfun,lmatch,goalopt) = function
@@ -708,14 +741,16 @@ let is_just_undef_macro ast =
       	(try let _ = Macros.lookup id in None with Not_found -> Some id)
     | _ -> None
 
-let vernac_interp =
+
+
+(*let vernac_interp =
   let gentac =
     hide_tactic "Interpret"
       (fun vargs gl -> match vargs with 
 	 | [Tacexp com] -> interp com gl
 	 | _ -> assert false) 
   in
-  fun com -> gentac [Tacexp com]
+  fun com -> gentac [Tacexp com]*)
 
 let vernac_interp_atomic =
   let gentac =
diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli
index 4405f0d228..39351dc1e5 100644
--- a/proofs/tacinterp.mli
+++ b/proofs/tacinterp.mli
@@ -37,7 +37,7 @@ val val_interp : interp_sign -> Coqast.t -> value
 val interp_tacarg : interp_sign -> Coqast.t -> tactic_arg
 
 val interp               : Coqast.t -> tactic
-val vernac_interp        : Coqast.t -> tactic
+(*val vernac_interp        : Coqast.t -> tactic*)
 val vernac_interp_atomic : identifier -> tactic_arg list -> tactic
 
 val is_just_undef_macro  : Coqast.t -> string option
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index ac4287ecb8..9471b5d258 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -184,6 +184,9 @@ let w_hnf_constr wc c        = hnf_constr (w_env wc) (w_Underlying wc) c
 (* Tacticals re-exported from the Refiner module.*)
 (*************************************************)
 
+(* A special exception for levels for the Fail tactic *)
+exception FailError = Refiner.FailError
+
 let tclIDTAC         = tclIDTAC
 let tclORELSE        = tclORELSE
 let tclTHEN          = tclTHEN
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 0fb2caa34e..60be331742 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -113,6 +113,9 @@ val instantiate_pf_com : int -> Coqast.t -> pftreestate -> pftreestate
 
 (*s Tacticals re-exported from the Refiner module. *)
 
+(* A special exception for levels for the Fail tactic *)
+exception FailError of int
+
 val tclIDTAC         : tactic
 val tclORELSE        : tactic -> tactic -> tactic
 val tclTHEN          : tactic -> tactic -> tactic
@@ -128,7 +131,7 @@ val tclTRY           : tactic -> tactic
 val tclTHENTRY       : tactic -> 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
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. *)