repeat_tac

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

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