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

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index 96cd29606493ce1eac22b671ad6c8a389cd8ee99..1d4738d952029f98835a93fbefefe7af21516313 100644 (file)
--- 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