Pcond (frama-c-wp.Wp.Pcond)

val pretty : Conditions.sequent Qed.Plib.printer

val dump : Conditions.bundle Qed.Plib.printer

val dump_bundle : 
  ?clause:string ->
  ?goal:Lang.F.pred ->
  Conditions.bundle Qed.Plib.printer

val dump_sequence : 
  ?clause:string ->
  ?goal:Lang.F.pred ->
  Conditions.sequence Qed.Plib.printer

type env = Plang.Env.t

val alloc_hyp : 
  Plang.pool ->
  (Lang.F.var -> unit) ->
  Conditions.sequence ->
  unit

val alloc_seq : 
  Plang.pool ->
  (Lang.F.var -> unit) ->
  Conditions.sequent ->
  unit

Sequent Printer Engine. Uses the following CSS:

class engine : Plang.engine -> object ... end

class state : object ... end

class seqengine : state -> object ... end