From 3dadfa509ace9184e5cf33a46d44c48c6fbed31b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 16 Mar 2010 16:41:40 +0000 Subject: [PATCH] 1) intros cleans up the cache (because the context changes) and this means that the case of an empty list of under_inspection is possible 2) every time we merge goals we need to remove the currently under inspection goal from the list --- helm/software/components/ng_tactics/nnAuto.ml | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml index 96cd29606..1d4738d95 100644 --- a/helm/software/components/ng_tactics/nnAuto.ml +++ b/helm/software/components/ng_tactics/nnAuto.ml @@ -1148,7 +1148,14 @@ let rec auto_clusters ?(top=false) if depth = 0 then raise (Proved status) else let status = NTactics.merge_tac status in - auto_clusters flags signature (cache:cache) (depth-1) status + let cache = + let l,tree = cache.under_inspection in + match l with + | [] -> cache (* possible because of intros that cleans the cache *) + | a::tl -> let tree = rm_from_th a tree a in + {cache with under_inspection = tl,tree} + in + auto_clusters flags signature cache (depth-1) status else if List.length goals < 2 then auto_main flags signature cache depth status else @@ -1221,7 +1228,7 @@ auto_main flags signature (cache:cache) depth status: unit = let cache = let l,tree = cache.under_inspection in match l with - | [] -> assert false + | [] -> cache (* possible because of intros that cleans the cache *) | a::tl -> let tree = rm_from_th a tree a in {cache with under_inspection = tl,tree} in @@ -1230,6 +1237,13 @@ auto_main flags signature (cache:cache) depth status: unit = if depth > 0 && move_to_side depth status then let status = NTactics.merge_tac status in + let cache = + let l,tree = cache.under_inspection in + match l with + | [] -> cache (* possible because of intros that cleans the cache*) + | a::tl -> let tree = rm_from_th a tree a in + {cache with under_inspection = tl,tree} + in auto_clusters flags signature cache (depth-1) status else let ng = List.length goals in -- 2.39.2