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 ae2ecd21bee13519bcf64e0c9ce0f7c95dc762e9..55678ae755d2288ff85d84fd4ebe9020aba29f60 100644 (file)
--- 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"));