Functor Prover.Make

module Make: 
functor (Seq : Sigs.SEQUENT) -> Sigs.PROVER 
  with module Seq = Seq 
  with type rule_t = Proofrule.Make(Seq).t 
  with module Proof = Proof.Make(Seq)

type rule_t 

module Seq: Sigs.SEQUENT 

module Proof: Sigs.PROOF 

val last_search_depth : int Pervasives.ref

val idfs : int ->
       int -> rule_t -> rule_t -> Seq.t -> Proof.t option

val print_proof_stats : Proof.t -> unit

val melt_proof : Pervasives.out_channel -> Proof.t -> unit