Module Wp.Plang

module Plang: sig .. end

Lang Pretty-Printer

type scope = Qed.Engine.scope 

module Env: Qed.Engine.Env  with type term := term

type pool 

val pool : unit -> pool

val alloc_e : pool -> (Wp.Lang.F.var -> unit) -> Wp.Lang.F.term -> unit

val alloc_p : pool -> (Wp.Lang.F.var -> unit) -> Wp.Lang.F.pred -> unit

val alloc_xs : pool -> (Wp.Lang.F.var -> unit) -> Wp.Lang.F.Vars.t -> unit

val alloc_domain : pool -> Wp.Lang.F.Vars.t

val sanitizer : string -> string

type iformat = [ `Bin | `Dec | `Hex ] 

type rformat = [ `Double | `Float | `Ratio ] 

class engine : object .. end