X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Ftacticals.ml;h=b0a9f452eda2fef9b064517aa663a8c1b40eb3ae;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=827d58bbcf6630e1a0b808d5b3900e781f19214b;hpb=9e8c5d2163e701413517153f00a52dac1cd31ecd;p=helm.git

diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml
index 827d58bbc..b0a9f452e 100644
--- a/helm/ocaml/tactics/tacticals.ml
+++ b/helm/ocaml/tactics/tacticals.ml
@@ -159,54 +159,17 @@ struct
               (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) continuations))
           @ [ C.Merge ]))
 
-(*   let thens ~start ~continuations =
-   let thens ~start ~continuations status =
-   let output_status = S.apply_tactic start status in
-   let new_goals = S.goals output_status in
-    try
-     let output_status,goals =
-      List.fold_left2
-       (fun (output_status,goals) goal tactic ->
-         let status = S.focus goal output_status in
-         let output_status' = S.apply_tactic tactic status in
-         let new_goals' = S.goals output_status' in
-          (output_status',goals@new_goals')
-       ) (output_status,[]) new_goals continuations
-     in
-      S.set_goals output_status goals
-    with
-     Invalid_argument _ -> 
-      let debug = Printf.sprintf "thens: expected %i new goals, found %i"
-       (List.length continuations) (List.length new_goals)
-      in
-      raise (Fail debug)
-   in
-    S.mk_tactic (thens ~start ~continuations ) *)
-
   let then_ ~start ~continuation =
     S.mk_tactic
       (fun istatus ->
-        fold_eval istatus
-          [ C.Tactical (C.Tactic start);
-            C.Semicolon;
-            C.Tactical (C.Tactic continuation) ])
-
-(*   let then_ ~start ~continuation =
-   let then_ ~start ~continuation status =
-   let output_status = S.apply_tactic start status in
-   let new_goals = S.goals output_status in
-    let output_status,goals =
-     List.fold_left
-      (fun (output_status,goals) goal ->
-        let status = S.focus goal output_status in
-        let output_status' = S.apply_tactic continuation status in
-        let new_goals' = S.goals output_status' in
-         (output_status',goals@new_goals')
-      ) (output_status,[]) new_goals
-    in
-     S.set_goals output_status goals
-   in
-    S.mk_tactic (then_ ~start ~continuation) *)
+        let ostatus = C.eval (C.Tactical (C.Tactic start)) istatus in
+        let opened,closed = S.goals ostatus in
+         match opened with
+            [] -> ostatus
+          | _ ->
+            fold_eval (S.focus ~-1 ostatus)
+              [ C.Semicolon;
+                C.Tactical (C.Tactic continuation) ])
 
   let seq ~tactics =
     S.mk_tactic
@@ -215,12 +178,6 @@ struct
           (HExtlib.list_concat ~sep:[ C.Semicolon ]
             (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) tactics)))
 
-(*   let rec seq ~tactics =
-    match tactics with
-    | [] -> assert false
-    | [tac] -> tac
-    | hd :: tl -> then_ ~start:hd ~continuation:(seq ~tactics:tl) *)
-
   (* TODO: x debug: i due tatticali seguenti non contano quante volte hanno
    * applicato la tattica *)
 
@@ -243,18 +200,6 @@ struct
    let rec repeat_tactic ~tactic status =
     info (lazy "in repeat_tactic");
     try
-(*      let rec step output_status opened closed =
-       match opened with
-       | [] -> output_status, [], closed
-       | head :: tail -> 
-           let status = S.focus head output_status in
-           let output_status' = repeat_tactic ~tactic status in
-           let opened', closed' = S.goals output_status' in
-           let output_status'', opened'', closed'' =
-             step output_status' tail []
-           in
-           output_status'', opened' @ opened'', closed' @ closed''
-     in *)
      let output_status = S.apply_tactic tactic status in
      let opened, closed = S.goals output_status in
      let output_status, opened', closed' =
@@ -279,16 +224,6 @@ struct
      try 
       let output_status = S.apply_tactic tactic status in
       let opened, closed = S.goals output_status in
-(*       let rec step output_status goallist =
-       match goallist with
-          [] -> output_status, []
-        | head::tail -> 
-           let status = S.focus head output_status in
-           let output_status' = do_tactic ~n:(n-1) ~tactic status in
-           let goallist' = S.goals output_status' in 
-           let (output_status'', goallist'') = step output_status' tail in
-            output_status'', goallist'@goallist''
-      in *)
        let output_status, opened', closed' =
          step (do_tactic ~n:(n-1) ~tactic) output_status opened closed
        in
@@ -380,7 +315,7 @@ struct
   let mk_tactic f =
     ProofEngineTypes.mk_tactic
       (fun (proof, goal) as pstatus ->
-        let stack = [ [ 1, Stack.Open goal ], [], [], Stack.NoTag ] in
+        let stack = [ [ 1, Stack.Open goal ], [], [], `NoTag ] in
         let istatus = pstatus, stack in
 (*         let ostatus = f istatus in
         let ((proof, opened, _), _) = ostatus in *)