From 2296f013ab579eec9643cfbcc703daa31a61ac91 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 6 Jul 2005 12:08:43 +0000
Subject: [PATCH] now it doesn't try to apply a cleared hypothesis

---
 helm/ocaml/tactics/autoTactic.ml | 60 ++++++++++++++++++--------------
 1 file changed, 33 insertions(+), 27 deletions(-)

diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml
index d0a44c561..def804790 100644
--- a/helm/ocaml/tactics/autoTactic.ml
+++ b/helm/ocaml/tactics/autoTactic.ml
@@ -53,28 +53,34 @@ 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 =
-	  try
-	    let (subst,(proof, goal_list)) =
-              PT.apply_tac_verbose ~term:(C.Rel n) status  in
-            (* 
-	    let goal_list =
-              List.stable_sort (compare_goal_list proof) goal_list in 
-            *)
-	    Some (subst,(proof, goal_list))
-	  with 
-	    PET.Fail _ -> None in
-	(match res with
-	  Some res -> res::(find (n+1) tl)
-	| None -> find (n+1) tl)
+        let res =
+          (* we should check that the hypothesys has not been cleared *)
+          if List.nth context (ctxlen - n) = None then
+            None
+          else
+            try
+              let (subst,(proof, goal_list)) =
+                PT.apply_tac_verbose ~term:(C.Rel n) status  
+              in
+              (* 
+                 let goal_list =
+                   List.stable_sort (compare_goal_list proof) goal_list in 
+              *)
+              Some (subst,(proof, goal_list))
+            with 
+              PET.Fail _ -> None 
+        in
+        (match res with
+        | Some res -> res::(find (n+1) tl)
+        | None -> find (n+1) tl)
   in
   try 
     find 1 context
-  with Failure s -> 
-    []
+  with Failure s -> []
 ;;     
 
 
@@ -117,7 +123,7 @@ let is_in_metasenv goal metasenv =
     let (_, ey ,ty) =
       CicUtil.lookup_meta goal metasenv in
       true
-  with _ -> false 
+  with CicUtil.Meta_not_found _ -> false 
 
 let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
  universe
@@ -223,21 +229,21 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
     end
       
 and auto_new dbd width already_seen_goals universe = function
-    [] -> []
+  | [] -> []
   | (subst,(proof, goals, sign))::tl ->
       let _,metasenv,_,_ = proof in
       let is_in_metasenv (goal, _) =
-	try
-	  let (_, ey ,ty) =
-	    CicUtil.lookup_meta goal metasenv in
-	    true
-	with _ -> false in
+        try
+          let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
+          true
+        with CicUtil.Meta_not_found _ -> false 
+      in
       let goals'= List.filter is_in_metasenv goals in
-	auto_new_aux dbd width already_seen_goals universe
-	  ((subst,(proof, goals', sign))::tl)
+    	auto_new_aux dbd 
+        width already_seen_goals universe ((subst,(proof, goals', sign))::tl)
 
 and auto_new_aux dbd width already_seen_goals universe = function
-  [] -> []
+  | [] -> []
   | (subst,(proof, [], sign))::tl -> (subst,(proof, [], sign))::tl
   | (subst,(proof, (goal,0)::_, _))::tl -> 
       auto_new dbd width already_seen_goals universe tl
-- 
2.39.2