X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FautoTactic.ml;h=03dd1f254487fbb0805f8933ef317b494f9df7ae;hb=33581c2ba6d8414968f4d3375352526ebf831a68;hp=b232d9894c444fb1ea2b431ff3811908e033930f;hpb=8b55faddb06e3c4b0a13839210bb49170939b33e;p=helm.git

diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml
index b232d9894..03dd1f254 100644
--- a/helm/ocaml/tactics/autoTactic.ml
+++ b/helm/ocaml/tactics/autoTactic.ml
@@ -120,13 +120,6 @@ let new_search_theorems f dbd proof goal depth sign =
 
 exception NoOtherChoices;;
 
-let is_in_metasenv goal metasenv =
-  try
-    let (_, ey ,ty) =
-      CicUtil.lookup_meta goal metasenv in
-      true
-  with CicUtil.Meta_not_found _ -> false 
-
 let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
  universe
   =
@@ -137,7 +130,7 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
   let _,metasenv,p,_ = proof in
     (* first of all we check if the goal has been already
        inspected *)
-  assert (is_in_metasenv goal metasenv);
+  assert (CicUtil.exists_meta goal metasenv);
   let exitus =
     try Hashtbl.find inspected_goals ty
     with Not_found -> NotYetInspected in
@@ -234,13 +227,9 @@ 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 CicUtil.Meta_not_found _ -> false 
+      let goals'=
+        List.filter (fun (goal, _) -> CicUtil.exists_meta goal metasenv) goals
       in
-      let goals'= List.filter is_in_metasenv goals in
     	auto_new_aux dbd 
         width already_seen_goals universe ((subst,(proof, goals', sign))::tl)