From 7daacec4a770f317d9c68c087bf93f1454d0e765 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 28 May 2007 17:16:43 +0000 Subject: [PATCH] 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. --- components/tactics/auto.ml | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) 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")); -- 2.39.2