From 2bd307bda75f4aee3b95c3d5039c64b34408dc6c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 14 Apr 2004 14:11:52 +0000 Subject: [PATCH] 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! --- helm/ocaml/tactics/variousTactics.ml | 21 +++++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) 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 -> -- 2.39.2