Fixed a bug in the "do" tactical that made it diverge.

diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml
index b5a45dae15d9c957a4fe21a14a1c4b177b241076..934b88a5ab6b1ebb0fccbdc8564cb8bff0bcd56f 100644 (file)
--- 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)