From 8464b71fdd68fade06484512b31077ff1a5a796a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 8 Jul 2009 16:16:06 +0000 Subject: [PATCH] repeat_tac --- helm/software/components/ng_tactics/nTactics.ml | 5 +++++ helm/software/components/ng_tactics/nTactics.mli | 1 + 2 files changed, 6 insertions(+) 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 -- 2.39.2