X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FautoTactic.ml;h=568e12ca40c4b303bd182ea3688efba78070ea0f;hb=12cc5b2b8e7f7bb0b5e315094b008a293a4df6b1;hp=def8047901aaf9ced990e9b66af64debeb8149bf;hpb=2296f013ab579eec9643cfbcc703daa31a61ac91;p=helm.git

diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml
index def804790..568e12ca4 100644
--- a/helm/ocaml/tactics/autoTactic.ml
+++ b/helm/ocaml/tactics/autoTactic.ml
@@ -53,13 +53,12 @@ let search_theorems_in_context status =
   let module PT = PrimitiveTactics in 
   let _,metasenv,_,_ = proof in
   let _,context,ty = CicUtil.lookup_meta goal metasenv in
-  let ctxlen = List.length context in
   let rec find n = function 
     | [] -> []
     | hd::tl ->
         let res =
           (* we should check that the hypothesys has not been cleared *)
-          if List.nth context (ctxlen - n) = None then
+          if List.nth context (n-1) = None then
             None
           else
             try
@@ -72,7 +71,7 @@ let search_theorems_in_context status =
               *)
               Some (subst,(proof, goal_list))
             with 
-              PET.Fail _ -> None 
+             PET.Fail _ -> None 
         in
         (match res with
         | Some res -> res::(find (n+1) tl)