X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=596a74e2e5fa1a837c7335a8faf3233462dedd6d;hb=4dc87cc7384ba61136bc82a23effe6a52160e720;hp=e044cd3bf2d194a467036480d6fe0525904c2515;hpb=1756fda18552874b063459b27448a4d0face1f39;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index e044cd3bf..596a74e2e 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -157,6 +157,7 @@ let block_tac l status =
   List.fold_left (fun status tac -> tac status) status l
 ;;
 
+
 let compare_statuses ~past ~present =
  let _,_,past,_,_ = past#obj in 
  let _,_,present,_,_ = present#obj in 
@@ -228,7 +229,16 @@ let distribute_tac tac (status : #tac_status) =
        ((status#set_stack stack)#set_obj(sn:>lowtac_status)#obj)#set_estatus sn
 ;;
 
-let atomic_tac htac = distribute_tac (exec htac) ;;
+let atomic_tac htac : #tac_status as 'a -> 'a = distribute_tac (exec htac) ;;
+
+let repeat_tac t s = 
+  let rec repeat t (status : #tac_status as 'a) : 'a = 
+    try repeat t (t status)
+    with NTacStatus.Error _ -> status
+  in
+    atomic_tac (repeat t) s
+;;
+
 
 let try_tac tac status =
   try
@@ -614,7 +624,3 @@ let auto_tac ~params status =
   distribute_tac (auto ~params) status
 ;;
 
-let rec repeat_tac t status =
-  try repeat_tac t (atomic_tac t status)
-  with NTacStatus.Error _ -> status
-;;