X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Ftacticals.mli;h=cdc3bac77f3557b4bc2b65ccb517892be45290e6;hb=b8f54b66890a55cfc255fa1df3e40fe60b78ee15;hp=a1b8ec7cd3e272af6f107344c81fc14620aec611;hpb=84d34c4d0b0a3c923a62cb686966ef66bccb54c8;p=helm.git

diff --git a/components/tactics/tacticals.mli b/components/tactics/tacticals.mli
index a1b8ec7cd..cdc3bac77 100644
--- a/components/tactics/tacticals.mli
+++ b/components/tactics/tacticals.mli
@@ -28,14 +28,14 @@ type tactic = ProofEngineTypes.tactic
 val id_tac : tactic
 val fail_tac: tactic
 
-val first: tactics: (string * tactic) list -> tactic
+val first: tactics: tactic list -> tactic
 val thens: start: tactic -> continuations: tactic list -> tactic
 val then_: start: tactic -> continuation: tactic -> tactic
 val seq: tactics: tactic list -> tactic (** "folding" of then_ *)
 val repeat_tactic: tactic: tactic -> tactic
 val do_tactic: n: int -> tactic: tactic -> tactic 
 val try_tactic: tactic: tactic -> tactic 
-val solve_tactics: tactics: (string * tactic) list -> tactic
+val solve_tactics: tactics: tactic list -> tactic
 val progress_tactic: tactic: tactic -> tactic 
 
 (* TODO temporary *)