sig   type cluster   val cluster :     id:string ->     ?title:string -> ?position:Lexing.position -> unit -> Definitions.cluster   val axiomatic : LogicUsage.axiomatic -> Definitions.cluster   val section : LogicUsage.logic_section -> Definitions.cluster   val compinfo : Cil_types.compinfo -> Definitions.cluster   val matrix : Ctypes.c_object -> Definitions.cluster   val cluster_id : Definitions.cluster -> string   val cluster_title : Definitions.cluster -> string   val cluster_position : Definitions.cluster -> Lexing.position option   val cluster_age : Definitions.cluster -> int   val cluster_compare : Definitions.cluster -> Definitions.cluster -> int   val pp_cluster : Format.formatter -> Definitions.cluster -> unit   val iter : (Definitions.cluster -> unit) -> unit   type trigger = (Lang.F.var, Lang.lfun) Qed.Engine.ftrigger   type typedef = (Lang.F.tau, Lang.field, Lang.lfun) Qed.Engine.ftypedef   type dlemma = {     l_name : string;     l_cluster : Definitions.cluster;     l_assumed : bool;     l_types : int;     l_forall : Lang.F.var list;     l_triggers : Definitions.trigger list list;     l_lemma : Lang.F.pred;   }   type definition =       Logic of Lang.F.tau     | Value of Lang.F.tau * Definitions.recursion * Lang.F.term     | Predicate of Definitions.recursion * Lang.F.pred     | Inductive of Definitions.dlemma list   and recursion = Def | Rec   type dfun = {     d_lfun : Lang.lfun;     d_cluster : Definitions.cluster;     d_types : int;     d_params : Lang.F.var list;     d_definition : Definitions.definition;   }   module Trigger :     sig       val of_term : Lang.F.term -> Definitions.trigger       val of_pred : Lang.F.pred -> Definitions.trigger       val vars : Definitions.trigger -> Lang.F.Vars.t     end   val define_symbol : Definitions.dfun -> unit   val update_symbol : Definitions.dfun -> unit   val find_lemma : LogicUsage.logic_lemma -> Definitions.dlemma   val compile_lemma :     (LogicUsage.logic_lemma -> Definitions.dlemma) ->     LogicUsage.logic_lemma -> unit   val define_lemma : Definitions.dlemma -> unit   val define_type : Definitions.cluster -> Cil_types.logic_type_info -> unit   val call_fun :     Lang.lfun ->     (Lang.lfun -> Definitions.dfun) -> Lang.F.term list -> Lang.F.term   val call_pred :     Lang.lfun ->     (Lang.lfun -> Definitions.dfun) -> Lang.F.term list -> Lang.F.pred   type axioms = Definitions.cluster * LogicUsage.logic_lemma list   class virtual visitor :     Definitions.cluster ->     object       method do_local : Definitions.cluster -> bool       method virtual on_cluster : Definitions.cluster -> unit       method virtual on_comp :         Cil_types.compinfo -> (Lang.field * Lang.F.tau) list -> unit       method virtual on_dfun : Definitions.dfun -> unit       method virtual on_dlemma : Definitions.dlemma -> unit       method virtual on_library : string -> unit       method virtual on_type :         Cil_types.logic_type_info -> Definitions.typedef -> unit       method virtual 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 end