module Plang:sig..end
typescope =Qed.Engine.scope
module Env:Qed.Engine.Envwith type term := term
type pool
val pool : unit -> pool
val alloc_e : pool -> (Lang.F.var -> unit) -> Lang.F.term -> unit
val alloc_p : pool -> (Lang.F.var -> unit) -> Lang.F.pred -> unit
val alloc_xs : pool -> (Lang.F.var -> unit) -> Lang.F.Vars.t -> unit
val alloc_domain : pool -> Lang.F.Vars.t
class engine :object..end