sig
  val dump : Conditions.bundle Qed.Plib.printer
  val bundle : ?clause:string -> Conditions.bundle Qed.Plib.printer
  val sequence : ?clause:string -> Conditions.sequence Qed.Plib.printer
  val pretty : Conditions.sequent Qed.Plib.printer
  type env = Plang.Env.t
  val xmark_hyp :
    Plang.pool -> (Lang.F.var -> unit) -> Conditions.sequence -> unit
  val xmark_seq :
    Plang.pool -> (Lang.F.var -> unit) -> Conditions.sequent -> unit
  class engine :
    Plang.engine ->
    object
      method mark : Lang.F.marks -> Conditions.step -> unit
      method name : Pcond.env -> Lang.F.term -> string
      method pp_clause : string Qed.Plib.printer
      method pp_comment : string Qed.Plib.printer
      method pp_condition :
        step:Conditions.step -> Conditions.condition Qed.Plib.printer
      method pp_core : Lang.F.term Qed.Plib.printer
      method pp_definition :
        Format.formatter -> string -> Lang.F.term -> unit
      method pp_esequent : Pcond.env -> Conditions.sequent Qed.Plib.printer
      method pp_intro :
        step:Conditions.step ->
        clause:string -> ?dot:string -> Lang.F.pred Qed.Plib.printer
      method pp_name : string Qed.Plib.printer
      method pp_property : Property.t Qed.Plib.printer
      method pp_sequence :
        clause:string -> Conditions.sequence Qed.Plib.printer
      method pp_sequent : Conditions.sequent Qed.Plib.printer
      method pp_step : Conditions.step Qed.Plib.printer
      method pp_warning : Warning.t Qed.Plib.printer
    end
end