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 6a31bd3474a8eb29db4b5218d312addbad5608d8..e85b89b95fe4ddbe76fa3b5dd6340bdf893fae38 100644 (file)
--- 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