From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 30 Apr 2007 10:51:14 +0000 (+0000)
Subject: Even if we are at depth 0, we first check in the cache for a solution,
X-Git-Tag: make_still_working~6351
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c98a165ddf5c74bb70ffaa4dc65fe89c20dba8b1;p=helm.git

Even if we are at depth 0, we first check in the cache for a solution,
before failing. In the other case the assert false at line 76 of
autocache may fail.
---

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index e85b89b95..c7cffc8af 100644
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -854,10 +854,6 @@ let rec auto_main tables maxm context flags elems universe cache =
     let goalty = CicMetaSubst.apply_subst subst goalty in
 (*     else if not (is_in_prop context subst metasenv goalty) then Fail,cache *)
       (* FAILURE (euristic cut) *)
-    if depth <= 0 then
-	Fail (string_of_int goalno ^ "as depth <=0"),
-          tables,cache,maxm (*FAILURE(depth)*)
-      else
     match cache_examine cache goalty with
     | Failed_in d when d >= depth -> 
         Fail ("depth " ^ string_of_int d ^ ">=" ^ string_of_int depth),
@@ -898,7 +894,7 @@ let rec auto_main tables maxm context flags elems universe cache =
 	    elems, tables, cache, maxm, flags  
         in
         aux flags tables maxm cache elems
-    | _ -> Fail "??",tables,cache,maxm 
+    | _ -> Fail "depth = 0",tables,cache,maxm 
   in
     aux flags tables maxm cache elems