X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=596a74e2e5fa1a837c7335a8faf3233462dedd6d;hb=72cd94b68037956a70b98cfa54f316fd54e52bae;hp=a384d54d56259f89952a7a14f8d013022cee568a;hpb=d268de514258947484a22a106c220b102c611cc3;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index a384d54d5..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
@@ -613,3 +623,4 @@ let auto ~params:(l,_) status goal =
 let auto_tac ~params status =
   distribute_tac (auto ~params) status
 ;;
+