Definitions.DC.elt ->
object
  val mutable clusters : Definitions.DC.t
  val mutable comps : Definitions.DR.t
  val mutable dlemmas : Definitions.DS.t
  val mutable lemmas : Definitions.DS.t
  val mutable locals : Definitions.DC.t
  val mutable symbols : Definitions.DF.t
  val mutable terms : Lang.F.Tset.t
  val mutable theories : Definitions.DS.t
  val mutable types : Definitions.DT.t
  method do_local : Definitions.DC.elt -> bool
  method virtual on_cluster : Definitions.DC.elt -> unit
  method virtual on_comp :
    Definitions.DR.elt -> (Lang.field * Lang.F.tau) list -> unit
  method virtual on_dfun : Definitions.Symbol.data -> unit
  method virtual on_dlemma : Definitions.Lemma.data -> unit
  method virtual on_library : Lang.library -> unit
  method virtual on_type : Definitions.DT.elt -> Definitions.typedef -> unit
  method virtual section : string -> unit
  method set_local : Definitions.DC.elt -> unit
  method vadt : Lang.adt -> unit
  method vcluster : Definitions.DC.elt -> unit
  method vcomp : Definitions.DR.elt -> unit
  method private vdefinition : Definitions.definition -> unit
  method private vdfun : Definitions.Symbol.data -> unit
  method private vdlemma : Definitions.Lemma.data -> unit
  method vfield : Lang.F.Field.t -> unit
  method vgoal : Definitions.axioms option -> Lang.F.pred -> unit
  method vlemma : LogicUsage.logic_lemma -> unit
  method private vlfun : Definitions.Symbol.key -> unit
  method vlibrary : Lang.library -> unit
  method vparam : Lang.F.var -> unit
  method vpred : Lang.F.pred -> unit
  method private vproperties : Definitions.definition -> unit
  method vself : unit
  method vsymbol : Lang.F.Fun.t -> unit
  method vtau : Lang.tau -> unit
  method vterm : Lang.F.Tset.elt -> unit
  method private vtrigger : Definitions.trigger -> unit
  method vtype : Definitions.DT.elt -> unit
  method private vtypedef : Cil_types.logic_type_def option -> unit
end