Format.formatter ->
Definitions.cluster ->
object
  val mutable deps : ProverCoq.depend list
  method add_coqfile : string -> unit
  method do_local : Definitions.cluster -> bool
  method flush : ProverCoq.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