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