AMBDA-TYPES: some improvements. subst now fully exploited

[helm.git] / components / tactics / substTactic.ml

diff --git a/components/tactics/substTactic.ml b/components/tactics/substTactic.ml
index fd11631ac6343f4cb2368e1054e0210cfcbae1ed..ef2a297e1cfc81e32d9b42e84d294421eb4fd73e 100644 (file)
--- a/components/tactics/substTactic.ml
+++ b/components/tactics/substTactic.ml
@@ -154,11 +154,6 @@ let subst_tac =
    let try_tac tactic = T.try_tactic ~tactic 
    let then_tac start continuation = T.then_ ~start ~continuation 
 
-let rec repeat_tactic ~tactic =
-   try_tac (then_tac tactic (repeat_tactic ~tactic))
-
 let subst_tac = 
-   let subst_tac status =
-      PET.apply_tactic (repeat_tactic ~tactic:subst_tac) status
-   in 
-   PET.mk_tactic subst_tac
+   let tactic = T.repeat_tactic ~tactic:subst_tac in
+   T.try_tactic ~tactic