* 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 -> 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:
after:ProofEngineTypes.goal list ->
opened:ProofEngineTypes.goal list ->
ProofEngineTypes.goal list * ProofEngineTypes.goal list
-