From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 8 Jul 2009 16:16:06 +0000 (+0000)
Subject: repeat_tac
X-Git-Tag: make_still_working~3727
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8464b71fdd68fade06484512b31077ff1a5a796a;p=helm.git

repeat_tac
---

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index a384d54d5..e044cd3bf 100644
--- 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 ab049f1c3..c81b1dd0b 100644
--- 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