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