From 3064844b2f594cfce55c0140ecb4d15e35364486 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 7 Jul 2005 15:31:01 +0000 Subject: [PATCH] fixed auto when the context has some deleted hypothesis --- helm/ocaml/tactics/autoTactic.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) 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) -- 2.39.2