X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Ftactics%2Ftacticals.ml;h=0479264d45d5a82b165f6cdbb896d5c56b4b5374;hb=927b0dc91ca0369dd029c43ffe9258e17908fa38;hp=5ea64913d0debbeacac87bcd4673a060f134c88c;hpb=655906d74521fa49de332f54ec34bfc9d9744151;p=helm.git

diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml
index 5ea64913d..0479264d4 100644
--- a/helm/ocaml/tactics/tacticals.ml
+++ b/helm/ocaml/tactics/tacticals.ml
@@ -47,7 +47,6 @@ let id_tac =
  in 
   mk_tactic tac
 
-
   (**
     naive implementation of ORELSE tactical, try a sequence of tactics in turn:
     if one fails pass to the next one and so on, eventually raises (failure "no
@@ -110,9 +109,11 @@ let then_ ~start ~continuation =
  in
   mk_tactic (then_ ~start ~continuation)
 
-(* Galla *)
-(* si suppone che tutte le tattiche sollevino solamente Fail? *)
-
+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 *)
 
@@ -187,6 +188,7 @@ let try_tactic ~tactic =
   mk_tactic (try_tactic ~tactic)
 ;;
 
+let fail = mk_tactic (fun _ -> raise (Fail "fail tactical"))
 
 (* This tries tactics until one of them doesn't _solve_ the goal *)
 (* TODO: si puo' unificare le 2(due) chiamate ricorsive? *)