- new tactic subst removes simple non recursive equalities from the context

[helm.git] / helm / software / components / tactics / tacticals.ml

diff --git a/helm/software/components/tactics/tacticals.ml b/helm/software/components/tactics/tacticals.ml
index ceb2d2de88cb28fc8a7554ee87c1167e5c846af8..88e2f4b9e371a3ce156c71de33c765889781da50 100644 (file)
--- a/helm/software/components/tactics/tacticals.ml
+++ b/helm/software/components/tactics/tacticals.ml
@@ -242,7 +242,7 @@ struct
 
   (* This applies tactic and catches its possible failure *)
   let try_tactic ~tactic =
-   let rec try_tactic ~tactic status =
+   let try_tactic status =
     info (lazy "in Tacticals.try_tactic");
     try
      S.apply_tactic tactic status
@@ -252,7 +252,7 @@ struct
         "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e));
       S.apply_tactic S.id_tactic status
    in
-    S.mk_tactic (try_tactic ~tactic)
+    S.mk_tactic try_tactic
 
   (* This tries tactics until one of them doesn't _solve_ the goal *)
   (* TODO: si puo' unificare le 2(due) chiamate ricorsive? *)