sig
  class console : title:string -> Tactical.feedback
  type jscript = ProofScript.alternative list
  and alternative = private
      Prover of VCS.prover * VCS.result
    | Tactic of int * ProofScript.jtactic * ProofScript.jscript list
    | Error of string * Json.t
  and jtactic = {
    header : string;
    tactic : string;
    params : Json.t;
    select : Json.t;
  }
  val is_prover : ProofScript.alternative -> bool
  val is_tactic : ProofScript.alternative -> bool
  val a_prover : VCS.prover -> VCS.result -> ProofScript.alternative
  val a_tactic :
    ProofScript.jtactic ->
    ProofScript.jscript list -> ProofScript.alternative
  val pending : ProofScript.alternative -> int
  val status : ProofScript.jscript -> int
  val decode : Json.t -> ProofScript.jscript
  val encode : ProofScript.jscript -> Json.t
  val jtactic :
    title:string ->
    Tactical.tactical -> Tactical.selection -> ProofScript.jtactic
  val configure :
    ProofScript.jtactic ->
    Conditions.sequent -> (Tactical.tactical * Tactical.selection) option
  val json_of_selection : Tactical.selection -> Json.t
  val selection_of_json : Conditions.sequent -> Json.t -> Tactical.selection
  val selection_target : Json.t -> string
  val json_of_param :
    Tactical.tactical -> Tactical.parameter -> string * Json.t
  val param_of_json :
    Tactical.tactical ->
    Conditions.sequent -> Json.t -> Tactical.parameter -> unit
  val json_of_parameters : Tactical.tactical -> Json.t
  val parameters_of_json :
    Tactical.tactical -> Conditions.sequent -> Json.t -> unit
  val json_of_tactic : ProofScript.jtactic -> Json.t list -> Json.t
  val json_of_result : VCS.prover -> VCS.result -> Json.t
  val prover_of_json : Json.t -> VCS.prover option
  val result_of_json : Json.t -> VCS.result
end