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