sig
  val array : ?priority:float -> Tactical.selection -> Strategy.strategy
  val choice : ?priority:float -> Tactical.selection -> Strategy.strategy
  val absurd : ?priority:float -> Tactical.selection -> Strategy.strategy
  val contrapose : ?priority:float -> Tactical.selection -> Strategy.strategy
  val compound : ?priority:float -> Tactical.selection -> Strategy.strategy
  val cut :
    ?priority:float -> ?modus:bool -> Tactical.selection -> Strategy.strategy
  val filter : ?priority:float -> ?anti:bool -> unit -> Strategy.strategy
  val havoc : ?priority:float -> Tactical.selection -> Strategy.strategy
  val separated : ?priority:float -> Tactical.selection -> Strategy.strategy
  val instance :
    ?priority:float ->
    Tactical.selection -> Tactical.selection list -> Strategy.strategy
  val lemma :
    ?priority:float ->
    ?at:Tactical.selection ->
    string -> Tactical.selection list -> Strategy.strategy
  val intuition : ?priority:float -> Tactical.selection -> Strategy.strategy
  val range :
    ?priority:float ->
    Tactical.selection -> vmin:int -> vmax:int -> Strategy.strategy
  val split : ?priority:float -> Tactical.selection -> Strategy.strategy
  val definition : ?priority:float -> Tactical.selection -> Strategy.strategy
  val auto_split : Strategy.heuristic
  val auto_range : Strategy.heuristic
  module Range :
    sig
      type rg
      val compute : Conditions.sequence -> Auto.Range.rg
      val ranges : Auto.Range.rg -> (int * int) Lang.F.Tmap.t
      val bounds : Auto.Range.rg -> (int option * int option) Lang.F.Tmap.t
    end
  val t_absurd : Tactical.process
  val t_id : Tactical.process
  val t_finally : string -> Tactical.process
  val t_descr : string -> Tactical.process -> Tactical.process
  val t_split : ?pos:string -> ?neg:string -> Lang.F.pred -> Tactical.process
  val t_cut :
    ?by:string -> Lang.F.pred -> Tactical.process -> Tactical.process
  val t_case :
    Lang.F.pred -> Tactical.process -> Tactical.process -> Tactical.process
  val t_cases :
    ?complete:string ->
    (Lang.F.pred * Tactical.process) list -> Tactical.process
  val t_chain : Tactical.process -> Tactical.process -> Tactical.process
  val t_range :
    Lang.F.term ->
    int ->
    int ->
    upper:Tactical.process ->
    lower:Tactical.process -> range:Tactical.process -> Tactical.process
  val t_replace :
    ?equal:string ->
    src:Lang.F.term ->
    tgt:Lang.F.term -> Tactical.process -> Tactical.process
end