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