From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 28 May 2007 17:16:43 +0000 (+0000)
Subject: Bug fixed (hopefully without introducing new ones): when the user clicked in
X-Git-Tag: 0.4.95@7852~427
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7daacec4a770f317d9c68c087bf93f1454d0e765;p=helm.git

Bug fixed (hopefully without introducing new ones): when the user clicked in
AutoWin on a theorem that does not generate new goals, the hint was never
found and auto "immediately" failed.
---

diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml
index ae2ecd21b..55678ae75 100644
--- a/components/tactics/auto.ml
+++ b/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"));