sig   type category = Wp.Lang.lfun Qed.Logic.category   type kind = Z | R | I of Wp.Ctypes.c_int | F of Wp.Ctypes.c_float | A   val add_builtin :     string -> Wp.LogicBuiltins.kind list -> Wp.Lang.lfun -> unit   type driver   val driver : Wp.LogicBuiltins.driver Wp.Context.value   val create :     id:string ->     ?descr:string -> ?includes:string list -> unit -> Wp.LogicBuiltins.driver   val init :     id:string -> ?descr:string -> ?includes:string list -> unit -> unit   val id : Wp.LogicBuiltins.driver -> string   val descr : Wp.LogicBuiltins.driver -> string   val is_default : Wp.LogicBuiltins.driver -> bool   val compare : Wp.LogicBuiltins.driver -> Wp.LogicBuiltins.driver -> int   val find_lib : string -> string   val dependencies : string -> string list   val add_library : string -> string list -> unit   val add_alias :     string -> Wp.LogicBuiltins.kind list -> alias:string -> unit -> unit   val add_type :     string ->     library:string -> ?link:string Wp.Lang.infoprover -> unit -> unit   val add_ctor :     string ->     Wp.LogicBuiltins.kind list ->     library:string -> link:Qed.Engine.link Wp.Lang.infoprover -> unit -> unit   val add_logic :     Wp.LogicBuiltins.kind ->     string ->     Wp.LogicBuiltins.kind list ->     library:string ->     ?category:Wp.LogicBuiltins.category ->     link:Qed.Engine.link Wp.Lang.infoprover -> unit -> unit   val add_predicate :     string ->     Wp.LogicBuiltins.kind list ->     library:string -> link:string Wp.Lang.infoprover -> unit -> unit   val add_option :     driver_dir:string -> string -> string -> library:string -> string -> unit   val set_option :     driver_dir:string -> string -> string -> library:string -> string -> unit   type doption   val create_option :     (driver_dir:string -> string -> string) ->     string -> string -> Wp.LogicBuiltins.doption   val get_option : Wp.LogicBuiltins.doption -> library:string -> string list   type builtin = ACSLDEF | LFUN of Wp.Lang.lfun   val logic : Cil_types.logic_info -> Wp.LogicBuiltins.builtin   val ctor : Cil_types.logic_ctor_info -> Wp.LogicBuiltins.builtin   val constant : string -> Wp.LogicBuiltins.builtin   val dump : unit -> unit end