Bug fixed: the following happened.

Auto generated two goals.
Closing the first goal instantiated also the second goal.
But we were still iterating over the original list of goals ==> BOOM!

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 70952d84d5157d2d6a73f1aec8b89165261824f4..080ba224d2cdfc223cc819910874d02de707ee54 100644 (file)
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -74,10 +74,19 @@ else
 prerr_endline ("GOALLIST = " ^ string_of_int (List.length goallist));
        (try 
           List.fold_left 
-            (fun (proof,opengoals) goal ->
-              let newproof, newgoals = auto_tac mqi_handle (level-1) proof goal in
-              (newproof, newgoals@opengoals))
-          (proof,[]) goallist
+            (fun proof goal ->
+              (* It may happen that to close the first open goal
+                 also some other goals are closed *)
+              let _,metasenv,_,_ = proof in
+               if List.exists (fun (i,_,_) -> i = goal) metasenv then
+                let newproof =
+                 auto_tac mqi_handle (level-1) proof goal
+                in
+                 newproof
+               else
+                (* goal already closed *)
+                proof)
+          proof goallist
         with 
        | MaxDepth
         | NotApplicableTheorem ->
@@ -87,9 +96,9 @@ prerr_endline ("GOALLIST = " ^ string_of_int (List.length goallist));
 let auto_tac mqi_handle ~status:(proof,goal) = 
   prerr_endline "Entro in Auto";
   try 
-    let res = auto_tac mqi_handle depth proof goal in
+    let proof = auto_tac mqi_handle depth proof goal in
 prerr_endline "AUTO_TAC HA FINITO";
-    res
+    (proof,[])
   with 
   | MaxDepth -> assert false (* this should happens only if depth is 0 above *)
   | NotApplicableTheorem ->