Module Wp.Pcond

module Pcond: sig .. end


All-in-one printers


val dump : Wp.Conditions.bundle Qed.Plib.printer
val bundle : ?clause:string -> Wp.Conditions.bundle Qed.Plib.printer
val sequence : ?clause:string -> Wp.Conditions.sequence Qed.Plib.printer
val pretty : Wp.Conditions.sequent Qed.Plib.printer

Low-level API


type env = Wp.Plang.Env.t 
val alloc_hyp : Wp.Plang.pool -> (Wp.Lang.F.var -> unit) -> Wp.Conditions.sequence -> unit
val alloc_seq : Wp.Plang.pool -> (Wp.Lang.F.var -> unit) -> Wp.Conditions.sequent -> unit

Sequent Printer Engine. Uses the following CSS:
class engine : #Wp.Plang.engine -> object .. end
class state : object .. end
class sequence : #state -> object .. end