repeat_tac

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index a384d54d56259f89952a7a14f8d013022cee568a..e044cd3bf2d194a467036480d6fe0525904c2515 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -613,3 +613,8 @@ let auto ~params:(l,_) status goal =
 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
+;;

diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index ab049f1c34fdc3495536a45c97f0273580c84e2b..c81b1dd0bab0ae8e202d1dab47a1f9e5261df5ff 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -21,6 +21,7 @@ val focus_tac: int list -> 's NTacStatus.tactic
 val unfocus_tac: 's NTacStatus.tactic
 val skip_tac: 's NTacStatus.tactic
 val try_tac: 's NTacStatus.tactic -> 's NTacStatus.tactic
+val repeat_tac: NTacStatus.tac_status NTacStatus.tactic -> 's NTacStatus.tactic
 
 val distribute_tac:
  NTacStatus.lowtac_status NTacStatus.lowtactic -> 's NTacStatus.tactic