Format.formatter ->
Definitions.cluster ->
object
val mutable deps : ProverWhy3.depend list
method add_dfile : string -> unit
method add_extlib : string -> unit
method add_import : ?was:string -> string -> unit
method add_import2 : string -> string -> unit
method add_import3 : string -> string -> string -> unit
method do_local : Definitions.cluster -> bool
method flush : ProverWhy3.depend list
method hline : unit
method lines : unit
method on_cluster : Definitions.cluster -> unit
method on_comp :
Cil_types.compinfo -> (Lang.field * Lang.F.tau) list -> unit
method on_dfun : Definitions.dfun -> unit
method on_dlemma : Definitions.dlemma -> unit
method on_library : string -> unit
method on_type : Cil_types.logic_type_info -> Definitions.typedef -> unit
method paragraph : unit
method printf : ('a, Format.formatter, unit) format -> 'a
method section : string -> unit
method set_local : Definitions.cluster -> unit
method vadt : Lang.F.ADT.t -> unit
method vcluster : Definitions.cluster -> unit
method vcomp : Cil_types.compinfo -> unit
method vfield : Lang.F.Field.t -> unit
method vgoal : Definitions.axioms option -> Lang.F.pred -> unit
method vlemma : LogicUsage.logic_lemma -> unit
method vlibrary : string -> unit
method vparam : Lang.F.var -> unit
method vpred : Lang.F.pred -> unit
method vself : unit
method vsymbol : Lang.lfun -> unit
method vtau : Lang.F.tau -> unit
method vterm : Lang.F.term -> unit
method vtype : Cil_types.logic_type_info -> unit
end