Definitions.DC.elt ->
object
val mutable clusters : Definitions.DC.t
val mutable comps : DR.t
val mutable dlemmas : DS.t
val mutable lemmas : DS.t
val mutable locals : Definitions.DC.t
val mutable symbols : Definitions.DF.t
val mutable terms : Lang.F.Tset.t
val mutable theories : DS.t
val mutable types : DT.t
method do_local : Definitions.DC.elt -> bool
method virtual on_cluster : Definitions.DC.elt -> unit
method virtual on_comp : 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 : 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 : 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 : DT.elt -> unit
method private vtypedef : Cil_types.logic_type_def option -> unit
end