new nrepeat (and block '('...')' ) tactical

[helm.git] / helm / software / components / ng_tactics / nTactics.ml

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index e044cd3bf2d194a467036480d6fe0525904c2515..596a74e2e5fa1a837c7335a8faf3233462dedd6d 100644 (file)
--- 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
-;;