X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=55678ae755d2288ff85d84fd4ebe9020aba29f60;hb=ee97363f43be9f2555f073693a10eee43b9cc8d7;hp=ae2ecd21bee13519bcf64e0c9ce0f7c95dc762e9;hpb=65ee9c1280990d3a5ada086786900ca13431d7a1;p=helm.git

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index ae2ecd21b..55678ae75 100644
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -1244,7 +1244,18 @@ let auto_main tables maxm context flags universe cache elems =
   auto_context := context;
   let rec aux tables maxm flags cache (elems : status) =
 (*     pp_status context elems; *)
+(* DEBUGGING CODE: uncomment these two lines to stop execution at each iteration
+    auto_status := elems;
+    check_pause ();
+*)
     match elems with
+    | (m, s, size, don, todo, fl)::orlist as status when !hint <> None ->
+        (match !hint with
+        | Some i when condition_for_hint i todo ->
+            aux tables maxm flags cache orlist
+        | _ ->
+          hint := None;
+          aux tables maxm flags cache elems)
     | [] ->
         (* complete failure *)
         Gaveup (tables, cache, maxm)
@@ -1318,11 +1329,7 @@ let auto_main tables maxm context flags universe cache elems =
                 aux tables maxm flags cache ((m, s, size, don,todo, fl)::orlist)
             | Notfound 
             | Failed_in _ when depth > 0 -> 
-                (match !hint with
-                | Some i when condition_for_hint i todo ->
-                    aux tables maxm flags cache orlist
-                | _ -> hint := None;
-                    (* more depth or is the first time we see the goal *)
+                ( (* more depth or is the first time we see the goal *)
                     if prunable m s gty todo then
                       (debug_print (lazy(
                          "FAIL: LOOP: one father is equal"));