sig
  type clause = Goal of Lang.F.pred | Step of Conditions.step
  type process = Conditions.sequent -> (string * Conditions.sequent) list
  type status =
      Not_applicable
    | Not_configured
    | Applicable of Tactical.process
  type selection =
      Empty
    | Clause of Tactical.clause
    | Inside of Tactical.clause * Lang.F.term
    | Compose of Tactical.compose
  and compose = private
      Cint of Integer.t
    | Range of int * int
    | Code of Lang.F.term * string * Tactical.selection list
  val int : int -> Tactical.selection
  val cint : Integer.t -> Tactical.selection
  val range : int -> int -> Tactical.selection
  val compose : string -> Tactical.selection list -> Tactical.selection
  val get_int : Tactical.selection -> int option
  val destruct : Tactical.selection -> Tactical.selection list
  val head : Tactical.clause -> Lang.F.pred
  val is_empty : Tactical.selection -> bool
  val selected : Tactical.selection -> Lang.F.term
  val subclause : Tactical.clause -> Lang.F.pred -> bool
  val pp_clause : Format.formatter -> Tactical.clause -> unit
  val pp_selection : Format.formatter -> Tactical.selection -> unit
  type 'a field
  module Fmap :
    sig
      type t
      val create : unit -> Tactical.Fmap.t
      val get : Tactical.Fmap.t -> 'Tactical.field -> 'a
      val set : Tactical.Fmap.t -> 'Tactical.field -> '-> unit
    end
  type 'a named = {
    title : string;
    descr : string;
    vid : string;
    value : 'a;
  }
  type 'a range = { vmin : 'a option; vmax : 'a option; vstep : 'a; }
  type 'a browser = ('Tactical.named -> unit) -> Tactical.selection -> unit
  type parameter =
      Checkbox of bool Tactical.field
    | Spinner of int Tactical.field * int Tactical.range
    | Composer of Tactical.selection Tactical.field * (Lang.F.term -> bool)
    | Selector : 'Tactical.field * 'Tactical.named list *
        ('-> '-> bool) -> Tactical.parameter
    | Search : 'Tactical.named option Tactical.field *
        'Tactical.browser * (string -> 'a) -> Tactical.parameter
  val ident : 'Tactical.field -> string
  val default : 'Tactical.field -> 'a
  val signature : 'Tactical.field -> 'Tactical.named
  val checkbox :
    id:string ->
    title:string ->
    descr:string ->
    ?default:bool -> unit -> bool Tactical.field * Tactical.parameter
  val spinner :
    id:string ->
    title:string ->
    descr:string ->
    ?default:int ->
    ?vmin:int ->
    ?vmax:int ->
    ?vstep:int -> unit -> int Tactical.field * Tactical.parameter
  val selector :
    id:string ->
    title:string ->
    descr:string ->
    ?default:'->
    options:'Tactical.named list ->
    ?equal:('-> '-> bool) ->
    unit -> 'Tactical.field * Tactical.parameter
  val composer :
    id:string ->
    title:string ->
    descr:string ->
    ?default:Tactical.selection ->
    ?filter:(Lang.F.term -> bool) ->
    unit -> Tactical.selection Tactical.field * Tactical.parameter
  val search :
    id:string ->
    title:string ->
    descr:string ->
    browse:'Tactical.browser ->
    find:(string -> 'a) ->
    unit -> 'Tactical.named option Tactical.field * Tactical.parameter
  type 'a formatter = ('a, Format.formatter, unit) Pervasives.format -> 'a
  class type feedback =
    object
      method get_title : string
      method has_error : bool
      method interactive : bool
      method pool : Lang.F.pool
      method set_descr : 'Tactical.formatter
      method set_error : 'Tactical.formatter
      method set_title : 'Tactical.formatter
      method update_field :
        ?enabled:bool ->
        ?title:string ->
        ?tooltip:string ->
        ?range:bool ->
        ?vmin:int ->
        ?vmax:int ->
        ?filter:(Lang.F.term -> bool) -> 'Tactical.field -> unit
    end
  val at : Tactical.selection -> int option
  val mapi : (int -> int -> '-> 'b) -> 'a list -> 'b list
  val insert : ?at:int -> (string * Lang.F.pred) list -> Tactical.process
  val replace :
    at:int -> (string * Conditions.condition) list -> Tactical.process
  val split : (string * Lang.F.pred) list -> Tactical.process
  val rewrite :
    ?at:int ->
    (string * Lang.F.pred * Lang.F.term * Lang.F.term) list ->
    Tactical.process
  class type tactical =
    object
      method descr : string
      method get_field : 'Tactical.field -> 'a
      method id : string
      method params : Tactical.parameter list
      method reset : unit
      method select :
        Tactical.feedback -> Tactical.selection -> Tactical.status
      method set_field : 'Tactical.field -> '-> unit
      method title : string
    end
  class virtual make :
    id:string ->
    title:string ->
    descr:string ->
    params:Tactical.parameter list ->
    object
      method descr : string
      method get_field : 'Tactical.field -> 'a
      method id : string
      method params : Tactical.parameter list
      method reset : unit
      method virtual select :
        Tactical.feedback -> Tactical.selection -> Tactical.status
      method set_field : 'Tactical.field -> '-> unit
      method title : string
    end
  class type composer =
    object
      method arity : int
      method compute : Lang.F.term list -> Lang.F.term
      method descr : string
      method filter : Lang.F.term list -> bool
      method group : string
      method id : string
      method title : string
    end
  type t = Tactical.tactical
  val register : #Tactical.tactical -> unit
  val export : #Tactical.tactical -> Tactical.tactical
  val lookup : id:string -> Tactical.tactical
  val iter : (Tactical.tactical -> unit) -> unit
  val add_composer : #Tactical.composer -> unit
  val iter_composer : (Tactical.composer -> unit) -> unit
end