X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Ftacticals.mli;h=44a6ab4d9cffb0160bd1deaa1ae64359725e4363;hb=cf25aeb5fa2c00ebfe93454fbe33421d590506d4;hp=e8d245cd1bf1635a37c199f62c0caa8aa2437a1d;hpb=1b3f24947f19050f3947397e50a8d5ed3b61b71b;p=helm.git

diff --git a/helm/software/components/tactics/tacticals.mli b/helm/software/components/tactics/tacticals.mli
index e8d245cd1..44a6ab4d9 100644
--- a/helm/software/components/tactics/tacticals.mli
+++ b/helm/software/components/tactics/tacticals.mli
@@ -23,66 +23,22 @@
  * http://cs.unibo.it/helm/.
  *)
 
-val id_tac : ProofEngineTypes.tactic
-val fail_tac: ProofEngineTypes.tactic
-
-(* module type Status =
- sig
-|+    type external_input_status +|
-   type input_status
-   type output_status
-|+    type external_output_status +|
-
-|+    val internalize: external_input_status -> input_status
-   val externalize: output_status -> external_output_status +|
-
-   type tactic
-
-   val mk_tactic : (input_status -> output_status) -> tactic
-   val apply_tactic : tactic -> input_status -> output_status
-
-   val id_tac : tactic
-
-   val goals : output_status -> ProofEngineTypes.goal list
-   val get_stack : input_status -> stack
-   val set_stack : stack -> output_status -> output_status
-
-   val inject : input_status -> output_status
-   val focus : goal -> output_status -> input_status
- end *)
-
-module type T =
-sig
-  type tactic
-
-  val first: tactics: (string * 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
-
-(*   module C:
-  sig *)
-  val tactic: tactic -> tactic  (** apply tactic to all goal in env *)
-  val skip: tactic
-  val dot: tactic
-  val semicolon: tactic
-  val branch: tactic
-  val shift: tactic
-  val pos: int list -> tactic
-  val wildcard: tactic
-  val merge: tactic
-  val focus: int list -> tactic
-  val unfocus: tactic
-(*   end *)
-end
-
-module Make (S: Continuationals.Status) : T with type tactic = S.tactic
-
-include T with type tactic = ProofEngineTypes.tactic
+type tactic = ProofEngineTypes.tactic
+
+val id_tac : tactic
+val fail_tac: tactic
+
+val first: tactics: tactic list -> tactic
+val thens: start: tactic -> continuations: tactic list -> tactic
+val then_: start: tactic -> continuation: tactic -> tactic
+val ifs: start: tactic -> continuations: tactic list -> fail: tactic -> tactic
+val if_: start: tactic -> continuation: tactic -> fail: 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: tactic list -> tactic
+val progress_tactic: tactic: tactic -> tactic 
 
 (* TODO temporary *)
 val goals_diff:
@@ -90,4 +46,3 @@ val goals_diff:
   after:ProofEngineTypes.goal list ->
   opened:ProofEngineTypes.goal list ->
     ProofEngineTypes.goal list * ProofEngineTypes.goal list
-