From 6331afd00aa6c1fabb43a368c383311fd3a55be4 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 6 Jul 2005 16:30:03 +0000
Subject: [PATCH] Fixed a bug in the "do" tactical that made it diverge.

---
 helm/ocaml/tactics/tacticals.ml | 46 ++++++++++++++++-----------------
 1 file changed, 22 insertions(+), 24 deletions(-)

diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml
index b5a45dae1..934b88a5a 100644
--- a/helm/ocaml/tactics/tacticals.ml
+++ b/helm/ocaml/tactics/tacticals.ml
@@ -208,30 +208,28 @@ let repeat_tactic ~tactic =
 (* This tries to apply tactic n times *)
 let do_tactic ~n ~tactic =
  let rec do_tactic ~n ~tactic status =
-  warn "in do_tactic";
-  try 
-   let output_status = 
-    if (n>0) then S.apply_tactic tactic status 
-             else S.apply_tactic S.id_tac status in
-   let goallist = S.goals output_status in
-(*             else (proof, []) in *)
-(* perche' non va bene questo? stessa questione di ##### ? *)
-   let rec step output_status goallist =
-    match goallist with
-       [] -> output_status, []
-     | head::tail -> 
-        let status = S.focus output_status head in
-        let output_status' = do_tactic ~n:(n-1) ~tactic status in
-        let goallist' = S.goals output_status' in 
-        let (output_status'', goallist'') = step output_status' tail in
-         output_status'', goallist'@goallist''
-   in
-    let output_status,goals = step output_status goallist in
-     S.set_goals output_status goals
-  with 
-   (Fail _) as e ->
-    warn ("Tacticals.do_tactic failed after nth time with exception: " ^ Printexc.to_string e) ;
-    S.apply_tactic S.id_tac status
+  if n = 0 then
+   S.apply_tactic S.id_tac status
+  else
+   try 
+    let output_status = S.apply_tactic tactic status in
+    let goallist = S.goals output_status in
+    let rec step output_status goallist =
+     match goallist with
+        [] -> output_status, []
+      | head::tail -> 
+         let status = S.focus output_status head in
+         let output_status' = do_tactic ~n:(n-1) ~tactic status in
+         let goallist' = S.goals output_status' in 
+         let (output_status'', goallist'') = step output_status' tail in
+          output_status'', goallist'@goallist''
+    in
+     let output_status,goals = step output_status goallist in
+      S.set_goals output_status goals
+   with 
+    (Fail _) as e ->
+     warn ("Tacticals.do_tactic failed after nth time with exception: " ^ Printexc.to_string e) ;
+     S.apply_tactic S.id_tac status
  in
   S.mk_tactic (do_tactic ~n ~tactic)
 
-- 
2.39.2