sig
  val occurs_x : Wp.Lang.F.var -> Wp.Lang.F.term -> bool
  val occurs_y : Wp.Lang.F.var -> Wp.Lang.F.pred -> bool
  val occurs_e : Wp.Lang.F.term -> Wp.Lang.F.term -> bool
  val occurs_p : Wp.Lang.F.term -> Wp.Lang.F.pred -> bool
  val occurs_q : Wp.Lang.F.pred -> Wp.Lang.F.pred -> bool
  val select_e :
    Wp.Conditions.sequent -> Wp.Lang.F.term -> Wp.Tactical.selection
  val select_p :
    Wp.Conditions.sequent -> Wp.Lang.F.pred -> Wp.Tactical.selection
  type argument = ARG : 'Wp.Tactical.field * '-> Wp.Strategy.argument
  type strategy = {
    priority : float;
    tactical : Wp.Tactical.tactical;
    selection : Wp.Tactical.selection;
    arguments : Wp.Strategy.argument list;
  }
  class pool :
    object
      method add : Wp.Strategy.strategy -> unit
      method sort : Wp.Strategy.strategy array
    end
  class type heuristic =
    object
      method descr : string
      method id : string
      method search :
        (Wp.Strategy.strategy -> unit) -> Wp.Conditions.sequent -> unit
      method title : string
    end
  val register : #Wp.Strategy.heuristic -> unit
  val export : #Wp.Strategy.heuristic -> Wp.Strategy.heuristic
  val lookup : id:string -> Wp.Strategy.heuristic
  val iter : (Wp.Strategy.heuristic -> unit) -> unit
  type t = Wp.Strategy.strategy
  val arg : 'Wp.Tactical.field -> '-> Wp.Strategy.argument
  val make :
    Wp.Tactical.tactical ->
    ?priority:float ->
    ?arguments:Wp.Strategy.argument list ->
    Wp.Tactical.selection -> Wp.Strategy.strategy
  val set_arg : Wp.Tactical.tactical -> Wp.Strategy.argument -> unit
  val set_args : Wp.Tactical.tactical -> Wp.Strategy.argument list -> unit
end