From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 30 Apr 2007 10:31:15 +0000 (+0000)
Subject: Removed an assert false; everything works again, but something
X-Git-Tag: 0.4.95@7852~493
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8a7a410e8829c66c9cc70d11e2cd7d9abd55b6da;p=helm.git

Removed an assert false; everything works again, but something
is clearly wrong (to be fixed).
---

diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml
index 6a31bd347..e85b89b95 100644
--- a/components/tactics/auto.ml
+++ b/components/tactics/auto.ml
@@ -745,7 +745,8 @@ let is_a_green_cut goalty =
   CicUtil.is_meta_closed goalty
 ;;
 
-let prop = function (_,_,P) -> true | _ -> false;;
+let prop = function (_,depth,P) -> depth < 9 | _ -> false;;
+
 let calculate_timeout flags = 
     if flags.timeout = 0. then 
       (prerr_endline "AUTO WITH NO TIMEOUT";{flags with timeout = infinity})
@@ -790,10 +791,12 @@ let rec auto_main tables maxm context flags elems universe cache =
         try
           let _,cc,goalty = CicUtil.lookup_meta goalno metasenv in
           debug_print 
-	    (lazy ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty));
+	    (lazy ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty ^
+                   "with depth"^string_of_int depth));
           debug_print (lazy (AutoCache.cache_print context cache));
           if sort = T (* && tl <> []*)  then 
-	  Success (metasenv,subst,tl), tables, cache,maxm 
+          aux flags tables maxm cache ((metasenv,subst,gl)::tl)
+	  (* Success (metasenv,subst,tl), tables, cache,maxm *)
           (*
             (debug_print 
 	       (lazy (" FAILURE(not in prop)"));
@@ -847,6 +850,7 @@ let rec auto_main tables maxm context flags elems universe cache =
           aux flags tables maxm cache ((metasenv,subst,gl)::tl)
 
   and aux_single flags tables maxm universe cache metasenv subst (goalno, depth, _) goalty cc =
+    (* let flags = if depth < 10 then {flags with maxwidth=3} else flags in *)
     let goalty = CicMetaSubst.apply_subst subst goalty in
 (*     else if not (is_in_prop context subst metasenv goalty) then Fail,cache *)
       (* FAILURE (euristic cut) *)
@@ -865,7 +869,9 @@ let rec auto_main tables maxm context flags elems universe cache =
         let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
         debug_print (lazy ("  CACHE HIT!"));
         Success (metasenv, subst, []), tables, cache, maxm
-    | UnderInspection -> Fail "looping",tables,cache, maxm
+    | UnderInspection -> 
+	(* assert (not (is_a_green_cut goalty)); *)
+	Fail "looping",tables,cache, maxm
     | Notfound 
     | Failed_in _ when depth > 0 -> (* we have more depth now *)
         let cache = cache_add_underinspection cache goalty depth in