- tacticals: new tactical ifs added: uses thens where if_ uses then_

[helm.git] / components / tactics / tacticals.mli

diff --git a/components/tactics/tacticals.mli b/components/tactics/tacticals.mli
index e8d245cd1bf1635a37c199f62c0caa8aa2437a1d..44a6ab4d9cffb0160bd1deaa1ae64359725e4363 100644 (file)
--- a/components/tactics/tacticals.mli
+++ b/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
-