better implementation of if_

diff --git a/helm/software/components/tactics/tacticals.ml b/helm/software/components/tactics/tacticals.ml
index cf5f22206d75faa5463932311a3c3b13625f2544..d5ec8acfb8be6c9edee7f353ba9f5368f8314511 100644 (file)
--- a/helm/software/components/tactics/tacticals.ml
+++ b/helm/software/components/tactics/tacticals.ml
@@ -180,29 +180,26 @@ let seq ~tactics =
         (HExtlib.list_concat ~sep:[ C.Semicolon ]
           (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) tactics)))
 
+(* Tacticals that cannot be implemented on top of tynycals *)
+
+let const_tac res = PET.mk_tactic (fun _ -> res)
+
 let if_ ~start ~continuation ~fail =
-  S.mk_tactic
-    (fun istatus -> 
-      let xostatus = 
-         try 
-           let res = C.eval (C.Tactical (C.Tactic start)) istatus in
+   let if_ status =
+      let xoutput = 
+         try
+           let result = PET.apply_tactic start status in
            info (lazy ("Tacticals.if_: succedeed!!!"));
-           Some res
+           Some result 
         with PET.Fail _ -> None
       in
-      match xostatus with
-         | Some ostatus ->
-            let opened,closed = S.goals ostatus in
-            begin match opened with
-                | [] -> ostatus
-                | _ ->
-                   fold_eval (S.focus ~-1 ostatus)
-                      [ C.Semicolon; C.Tactical (C.Tactic continuation) ]
-            end
-        | None -> C.eval (C.Tactical (C.Tactic fail)) istatus
-    )
-
-(* Tacticals that cannot be implemented on top of tynycals *)
+      let tactic = match xoutput with
+         | Some res -> then_ ~start:(const_tac res) ~continuation
+        | None     -> fail
+      in 
+      PET.apply_tactic tactic status
+   in
+   PET.mk_tactic if_
 
 let first ~tactics =
   let rec first ~(tactics: tactic list) status =
@@ -219,7 +216,6 @@ let first ~tactics =
   in
   PET.mk_tactic (first ~tactics)
 
-
 let rec do_tactic ~n ~tactic =
  PET.mk_tactic
   (function status ->