#Wp.Plang.engine ->
object
  method mark : Wp.Lang.F.marks -> Wp.Conditions.step -> unit
  method name : Wp.Pcond.env -> Wp.Lang.F.term -> string
  method pp_block : clause:string -> Wp.Conditions.sequence Qed.Plib.printer
  method pp_clause : string Qed.Plib.printer
  method pp_comment : string Qed.Plib.printer
  method pp_condition :
    step:Wp.Conditions.step -> Wp.Conditions.condition Qed.Plib.printer
  method pp_core : Wp.Lang.F.term Qed.Plib.printer
  method pp_definition : Format.formatter -> string -> Wp.Lang.F.term -> unit
  method pp_esequent : Wp.Pcond.env -> Wp.Conditions.sequent Qed.Plib.printer
  method pp_goal : Wp.Lang.F.pred Qed.Plib.printer
  method pp_intro :
    step:Wp.Conditions.step ->
    clause:string -> ?dot:string -> Wp.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 -> Wp.Conditions.sequence Qed.Plib.printer
  method pp_sequent : Wp.Conditions.sequent Qed.Plib.printer
  method pp_step : Wp.Conditions.step Qed.Plib.printer
  method pp_stmt : string Qed.Plib.printer
  method pp_warning : Wp.Warning.t Qed.Plib.printer
end