From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 14 Apr 2004 14:11:52 +0000 (+0000)
Subject: Bug fixed: the following happened.
X-Git-Tag: dead_dir_walking~68
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2bd307bda75f4aee3b95c3d5039c64b34408dc6c;p=helm.git

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 70952d84d..080ba224d 100644
--- 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 ->