sig   type library = string   type 'a infoprover = { altergo : 'a; why3 : 'a; coq : 'a; }   val infoprover : '-> 'Wp.Lang.infoprover   val comp_id : Cil_types.compinfo -> string   val field_id : Cil_types.fieldinfo -> string   val type_id : Cil_types.logic_type_info -> string   val logic_id : Cil_types.logic_info -> string   val lemma_id : string -> string   type adt = private       Mtype of Wp.Lang.mdt     | Mrecord of Wp.Lang.mdt * Wp.Lang.fields     | Atype of Cil_types.logic_type_info     | Comp of Cil_types.compinfo   and mdt = string Wp.Lang.extern   and 'a extern = {     ext_id : int;     ext_link : 'Wp.Lang.infoprover;     ext_library : Wp.Lang.library;     ext_debug : string;   }   and fields = { mutable fields : Wp.Lang.field list; }   and field =       Mfield of Wp.Lang.mdt * Wp.Lang.fields * string * Wp.Lang.tau     | Cfield of Cil_types.fieldinfo   and tau = (Wp.Lang.field, Wp.Lang.adt) Qed.Logic.datatype   type lfun =       ACSL of Cil_types.logic_info     | CTOR of Cil_types.logic_ctor_info     | Model of Wp.Lang.model   and model = {     m_category : Wp.Lang.lfun Qed.Logic.category;     m_params : Qed.Logic.sort list;     m_resort : Qed.Logic.sort;     m_result : Wp.Lang.tau option;     m_source : Wp.Lang.source;   }   and source = Generated of string | Extern of Qed.Engine.link Wp.Lang.extern   val builtin_type :     name:string -> link:string Wp.Lang.infoprover -> library:string -> unit   val is_builtin_type : name:string -> Wp.Lang.tau -> bool   val datatype : library:string -> string -> Wp.Lang.adt   val record :     link:string Wp.Lang.infoprover ->     library:string -> (string * Wp.Lang.tau) list -> Wp.Lang.adt   val atype : Cil_types.logic_type_info -> Wp.Lang.adt   val comp : Cil_types.compinfo -> Wp.Lang.adt   val field : Wp.Lang.adt -> string -> Wp.Lang.field   val fields_of_tau : Wp.Lang.tau -> Wp.Lang.field list   val fields_of_field : Wp.Lang.field -> Wp.Lang.field list   type balance = Nary | Left | Right   val extern_s :     library:Wp.Lang.library ->     ?link:Qed.Engine.link Wp.Lang.infoprover ->     ?category:Wp.Lang.lfun Qed.Logic.category ->     ?params:Qed.Logic.sort list ->     ?sort:Qed.Logic.sort -> ?result:Wp.Lang.tau -> string -> Wp.Lang.lfun   val extern_f :     library:Wp.Lang.library ->     ?link:Qed.Engine.link Wp.Lang.infoprover ->     ?balance:Wp.Lang.balance ->     ?category:Wp.Lang.lfun Qed.Logic.category ->     ?params:Qed.Logic.sort list ->     ?sort:Qed.Logic.sort ->     ?result:Wp.Lang.tau ->     ('a, Format.formatter, unit, Wp.Lang.lfun) Pervasives.format4 -> 'a   val extern_p :     library:Wp.Lang.library ->     ?bool:string ->     ?prop:string ->     ?link:Qed.Engine.link Wp.Lang.infoprover ->     ?params:Qed.Logic.sort list -> unit -> Wp.Lang.lfun   val extern_fp :     library:Wp.Lang.library ->     ?params:Qed.Logic.sort list ->     ?link:string Wp.Lang.infoprover -> string -> Wp.Lang.lfun   val generated_f :     ?category:Wp.Lang.lfun Qed.Logic.category ->     ?params:Qed.Logic.sort list ->     ?sort:Qed.Logic.sort ->     ?result:Wp.Lang.tau ->     ('a, Format.formatter, unit, Wp.Lang.lfun) Pervasives.format4 -> 'a   val generated_p : string -> Wp.Lang.lfun   val tau_of_comp : Cil_types.compinfo -> Wp.Lang.tau   val tau_of_object : Wp.Ctypes.c_object -> Wp.Lang.tau   val tau_of_ctype : Cil_types.typ -> Wp.Lang.tau   val tau_of_ltype : Cil_types.logic_type -> Wp.Lang.tau   val tau_of_return : Cil_types.logic_info -> Wp.Lang.tau   val tau_of_lfun : Wp.Lang.lfun -> Wp.Lang.tau   val tau_of_field : Wp.Lang.field -> Wp.Lang.tau   val tau_of_record : Wp.Lang.field -> Wp.Lang.tau   val array : Wp.Lang.tau -> Wp.Lang.tau   val farray : Wp.Lang.tau -> Wp.Lang.tau -> Wp.Lang.tau   val pointer : (Cil_types.typ -> Wp.Lang.tau) Wp.Context.value   val poly : string list Wp.Context.value   val parameters : (Wp.Lang.lfun -> Qed.Logic.sort list) -> unit   module ADT :     sig       type t = adt       val hash : t -> int       val equal : t -> t -> bool       val compare : t -> t -> int       val pretty : Format.formatter -> t -> unit       val debug : t -> string       val basename : t -> string     end   module Field :     sig       type t = field       val hash : t -> int       val equal : t -> t -> bool       val compare : t -> t -> int       val pretty : Format.formatter -> t -> unit       val debug : t -> string       val sort : t -> Qed.Logic.sort     end   module Fun :     sig       type t = lfun       val hash : t -> int       val equal : t -> t -> bool       val compare : t -> t -> int       val pretty : Format.formatter -> t -> unit       val debug : t -> string       val category : t -> t Qed.Logic.category       val params : t -> Qed.Logic.sort list       val sort : t -> Qed.Logic.sort     end   class virtual idprinting :     object       method virtual basename : string -> string       method datatype : Wp.Lang.ADT.t -> string       method datatypename : string -> string       method field : Wp.Lang.Field.t -> string       method fieldname : string -> string       method funname : string -> string       method virtual infoprover : 'Wp.Lang.infoprover -> 'a       method link : Wp.Lang.Fun.t -> Qed.Engine.link     end   module F :     sig       module Z :         sig           type t = Integer.t           val zero : t           val one : t           val minus_one : t           val succ : t -> t           val pred : t -> t           val neg : t -> t           val add : t -> t -> t           val sub : t -> t -> t           val mul : t -> t -> t           val div : t -> t -> t           val rem : t -> t -> t           val div_rem : t -> t -> t * t           val equal : t -> t -> bool           val leq : t -> t -> bool           val lt : t -> t -> bool           val of_int : int -> t           val of_string : string -> t           val to_string : t -> string           val hash : t -> int           val compare : t -> t -> int         end       module ADT :         sig           type t = adt           val hash : t -> int           val equal : t -> t -> bool           val compare : t -> t -> int           val pretty : Format.formatter -> t -> unit           val debug : t -> string           val basename : t -> string         end       module Field :         sig           type t = field           val hash : t -> int           val equal : t -> t -> bool           val compare : t -> t -> int           val pretty : Format.formatter -> t -> unit           val debug : t -> string           val sort : t -> Qed.Logic.sort         end       module Fun :         sig           type t = lfun           val hash : t -> int           val equal : t -> t -> bool           val compare : t -> t -> int           val pretty : Format.formatter -> t -> unit           val debug : t -> string           val category : t -> t Qed.Logic.category           val params : t -> Qed.Logic.sort list           val sort : t -> Qed.Logic.sort         end       module Var : Qed.Logic.Variable       type term       type bind       type var = Var.t       type tau = (Field.t, ADT.t) Qed.Logic.datatype       type signature = (Field.t, ADT.t) Qed.Logic.funtype       module Tau :         sig           type t = tau           val hash : t -> int           val equal : t -> t -> bool           val compare : t -> t -> int           val pretty : Format.formatter -> t -> unit           val debug : t -> string           val basename : t -> string         end       module Vars :         sig           type elt = var           type t           val empty : t           val is_empty : t -> bool           val mem : elt -> t -> bool           val find : elt -> t -> elt           val add : elt -> t -> t           val singleton : elt -> t           val remove : elt -> t -> t           val union : t -> t -> t           val inter : t -> t -> t           val diff : t -> t -> t           val compare : t -> t -> int           val equal : t -> t -> bool           val subset : t -> t -> bool           val iter : (elt -> unit) -> t -> unit           val fold : (elt -> '-> 'a) -> t -> '-> 'a           val for_all : (elt -> bool) -> t -> bool           val exists : (elt -> bool) -> t -> bool           val filter : (elt -> bool) -> t -> t           val partition : (elt -> bool) -> t -> t * t           val cardinal : t -> int           val elements : t -> elt list           val map : (elt -> elt) -> t -> t           val mapf : (elt -> elt option) -> t -> t           val intersect : t -> t -> bool         end       module Vmap :         sig           type key = var           type 'a t           val is_empty : 'a t -> bool           val empty : 'a t           val add : key -> '-> 'a t -> 'a t           val mem : key -> 'a t -> bool           val find : key -> 'a t -> 'a           val remove : key -> 'a t -> 'a t           val compare : ('-> '-> int) -> 'a t -> 'a t -> int           val equal : ('-> '-> bool) -> 'a t -> 'a t -> bool           val iter : (key -> '-> unit) -> 'a t -> unit           val map : (key -> '-> 'b) -> 'a t -> 'b t           val mapf : (key -> '-> 'b option) -> 'a t -> 'b t           val mapq : (key -> '-> 'a option) -> 'a t -> 'a t           val filter : (key -> '-> bool) -> 'a t -> 'a t           val partition : (key -> '-> bool) -> 'a t -> 'a t * 'a t           val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b           val union : (key -> '-> '-> 'a) -> 'a t -> 'a t -> 'a t           val inter : (key -> '-> '-> 'c) -> 'a t -> 'b t -> 'c t           val interf : (key -> '-> '-> 'c option) -> 'a t -> 'b t -> 'c t           val interq : (key -> '-> '-> 'a option) -> 'a t -> 'a t -> 'a t           val diffq : (key -> '-> '-> 'a option) -> 'a t -> 'a t -> 'a t           val merge :             (key -> 'a option -> 'b option -> 'c option) ->             'a t -> 'b t -> 'c t           val insert : (key -> '-> '-> 'a) -> key -> '-> 'a t -> 'a t           val change :             (key -> '-> 'a option -> 'a option) ->             key -> '-> 'a t -> 'a t         end       type pool       val pool : ?copy:pool -> unit -> pool       val add_var : pool -> var -> unit       val add_vars : pool -> Vars.t -> unit       val add_term : pool -> term -> unit       val fresh : pool -> ?basename:string -> tau -> var       val alpha : pool -> var -> var       val tau_of_var : var -> tau       val sort_of_var : var -> Qed.Logic.sort       val base_of_var : var -> string       type 'a expression =           (Z.t, Field.t, ADT.t, Fun.t, var, bind, 'a) Qed.Logic.term_repr       type repr = term expression       type path = int list       type record = (Field.t * term) list       val decide : term -> bool       val is_true : term -> Qed.Logic.maybe       val is_false : term -> Qed.Logic.maybe       val is_prop : term -> bool       val is_int : term -> bool       val is_real : term -> bool       val is_arith : term -> bool       val are_equal : term -> term -> Qed.Logic.maybe       val eval_eq : term -> term -> bool       val eval_neq : term -> term -> bool       val eval_lt : term -> term -> bool       val eval_leq : term -> term -> bool       val repr : term -> repr       val sort : term -> Qed.Logic.sort       val vars : term -> Vars.t       val subterm : term -> path -> term       val change_subterm : term -> path -> term -> term       val e_true : term       val e_false : term       val e_bool : bool -> term       val e_literal : bool -> term -> term       val e_int : int -> term       val e_zint : Z.t -> term       val e_real : Qed.R.t -> term       val e_var : var -> term       val e_opp : term -> term       val e_times : Z.t -> term -> term       val e_sum : term list -> term       val e_prod : term list -> term       val e_add : term -> term -> term       val e_sub : term -> term -> term       val e_mul : term -> term -> term       val e_div : term -> term -> term       val e_mod : term -> term -> term       val e_eq : term -> term -> term       val e_neq : term -> term -> term       val e_leq : term -> term -> term       val e_lt : term -> term -> term       val e_imply : term list -> term -> term       val e_equiv : term -> term -> term       val e_and : term list -> term       val e_or : term list -> term       val e_not : term -> term       val e_if : term -> term -> term -> term       val e_get : term -> term -> term       val e_set : term -> term -> term -> term       val e_getfield : term -> Field.t -> term       val e_record : record -> term       val e_fun : Fun.t -> term list -> term       val e_repr : repr -> term       val e_forall : var list -> term -> term       val e_exists : var list -> term -> term       val e_lambda : var list -> term -> term       val e_bind : Qed.Logic.binder -> var -> term -> term       val e_apply : term -> term list -> term       type sigma       val sigma : unit -> sigma       val e_subst_var : var -> term -> term -> term       val lc_bind : var -> term -> bind       val lc_open : var -> bind -> term       val lc_open_term : term -> bind -> term       val lc_closed : term -> bool       val lc_closed_at : int -> term -> bool       val lc_vars : term -> Qed.Bvars.t       val lc_repr : bind -> term       val e_map : pool -> (term -> term) -> term -> term       val e_iter : pool -> (term -> unit) -> term -> unit       val f_map : (int -> term -> term) -> int -> term -> term       val f_iter : (int -> term -> unit) -> int -> term -> unit       val lc_map : (term -> term) -> term -> term       val lc_iter : (term -> unit) -> term -> unit       val set_builtin : Fun.t -> (term list -> term) -> unit       val set_builtin_eq : Fun.t -> (term -> term -> term) -> unit       val set_builtin_leq : Fun.t -> (term -> term -> term) -> unit       val consequence : term -> term -> term       val literal : term -> bool * term       val congruence_eq : term -> term -> (term * term) list option       val congruence_neq : term -> term -> (term * term) list option       val flattenable : term -> bool       val flattens : term -> term -> bool       val flatten : term -> term list       val affine : term -> (Z.t, term) Qed.Logic.affine       val record_with : record -> (term * record) option       type t = term       val id : t -> int       val hash : t -> int       val equal : t -> t -> bool       val compare : t -> t -> int       val pretty : Format.formatter -> t -> unit       val weigth : t -> int       val is_closed : t -> bool       val is_simple : t -> bool       val is_atomic : t -> bool       val is_primitive : t -> bool       val is_neutral : Fun.t -> t -> bool       val is_absorbant : Fun.t -> t -> bool       val size : t -> int       val basename : t -> string       val debug : Format.formatter -> t -> unit       val pp_id : Format.formatter -> t -> unit       val pp_rid : Format.formatter -> t -> unit       val pp_repr : Format.formatter -> repr -> unit       module Term :         sig           type t = term           val hash : t -> int           val equal : t -> t -> bool           val compare : t -> t -> int           val pretty : Format.formatter -> t -> unit           val debug : t -> string         end       module Tset :         sig           type elt = term           type t           val empty : t           val is_empty : t -> bool           val mem : elt -> t -> bool           val find : elt -> t -> elt           val add : elt -> t -> t           val singleton : elt -> t           val remove : elt -> t -> t           val union : t -> t -> t           val inter : t -> t -> t           val diff : t -> t -> t           val compare : t -> t -> int           val equal : t -> t -> bool           val subset : t -> t -> bool           val iter : (elt -> unit) -> t -> unit           val fold : (elt -> '-> 'a) -> t -> '-> 'a           val for_all : (elt -> bool) -> t -> bool           val exists : (elt -> bool) -> t -> bool           val filter : (elt -> bool) -> t -> t           val partition : (elt -> bool) -> t -> t * t           val cardinal : t -> int           val elements : t -> elt list           val map : (elt -> elt) -> t -> t           val mapf : (elt -> elt option) -> t -> t           val intersect : t -> t -> bool         end       module Tmap :         sig           type key = term           type 'a t           val is_empty : 'a t -> bool           val empty : 'a t           val add : key -> '-> 'a t -> 'a t           val mem : key -> 'a t -> bool           val find : key -> 'a t -> 'a           val remove : key -> 'a t -> 'a t           val compare : ('-> '-> int) -> 'a t -> 'a t -> int           val equal : ('-> '-> bool) -> 'a t -> 'a t -> bool           val iter : (key -> '-> unit) -> 'a t -> unit           val map : (key -> '-> 'b) -> 'a t -> 'b t           val mapf : (key -> '-> 'b option) -> 'a t -> 'b t           val mapq : (key -> '-> 'a option) -> 'a t -> 'a t           val filter : (key -> '-> bool) -> 'a t -> 'a t           val partition : (key -> '-> bool) -> 'a t -> 'a t * 'a t           val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b           val union : (key -> '-> '-> 'a) -> 'a t -> 'a t -> 'a t           val inter : (key -> '-> '-> 'c) -> 'a t -> 'b t -> 'c t           val interf : (key -> '-> '-> 'c option) -> 'a t -> 'b t -> 'c t           val interq : (key -> '-> '-> 'a option) -> 'a t -> 'a t -> 'a t           val diffq : (key -> '-> '-> 'a option) -> 'a t -> 'a t -> 'a t           val merge :             (key -> 'a option -> 'b option -> 'c option) ->             'a t -> 'b t -> 'c t           val insert : (key -> '-> '-> 'a) -> key -> '-> 'a t -> 'a t           val change :             (key -> '-> 'a option -> 'a option) ->             key -> '-> 'a t -> 'a t         end       val shared :         ?shared:(term -> bool) ->         ?shareable:(term -> bool) -> term list -> term list       type marks       val marks :         ?shared:(term -> bool) -> ?shareable:(term -> bool) -> unit -> marks       val mark : marks -> term -> unit       val share : marks -> term -> unit       val defs : marks -> term list       type unop = term -> term       type binop = term -> term -> term       val e_zero : term       val e_one : term       val e_minus_one : term       val e_one_real : term       val e_zero_real : term       val constant : term -> term       val e_fact : int -> term -> term       val e_int64 : int64 -> term       val e_bigint : Integer.t -> term       val e_mthfloat : float -> term       val e_hexfloat : float -> term       val e_setfield : term -> Wp.Lang.field -> term -> term       val e_range : term -> term -> term       val is_zero : term -> bool       type pred       type cmp = term -> term -> Wp.Lang.F.pred       val p_true : Wp.Lang.F.pred       val p_false : Wp.Lang.F.pred       val p_equal : term -> term -> Wp.Lang.F.pred       val p_neq : term -> term -> Wp.Lang.F.pred       val p_leq : term -> term -> Wp.Lang.F.pred       val p_lt : term -> term -> Wp.Lang.F.pred       val p_positive : term -> Wp.Lang.F.pred       val is_ptrue : Wp.Lang.F.pred -> Qed.Logic.maybe       val is_pfalse : Wp.Lang.F.pred -> Qed.Logic.maybe       val is_equal : term -> term -> Qed.Logic.maybe       val eqp : Wp.Lang.F.pred -> Wp.Lang.F.pred -> bool       val comparep : Wp.Lang.F.pred -> Wp.Lang.F.pred -> int       val p_bool : term -> Wp.Lang.F.pred       val e_prop : Wp.Lang.F.pred -> term       val p_bools : term list -> Wp.Lang.F.pred list       val e_props : Wp.Lang.F.pred list -> term list       val lift : (term -> term) -> Wp.Lang.F.pred -> Wp.Lang.F.pred       val p_not : Wp.Lang.F.pred -> Wp.Lang.F.pred       val p_and : Wp.Lang.F.pred -> Wp.Lang.F.pred -> Wp.Lang.F.pred       val p_or : Wp.Lang.F.pred -> Wp.Lang.F.pred -> Wp.Lang.F.pred       val p_imply : Wp.Lang.F.pred -> Wp.Lang.F.pred -> Wp.Lang.F.pred       val p_equiv : Wp.Lang.F.pred -> Wp.Lang.F.pred -> Wp.Lang.F.pred       val p_hyps : Wp.Lang.F.pred list -> Wp.Lang.F.pred -> Wp.Lang.F.pred       val p_if :         Wp.Lang.F.pred -> Wp.Lang.F.pred -> Wp.Lang.F.pred -> Wp.Lang.F.pred       val p_conj : Wp.Lang.F.pred list -> Wp.Lang.F.pred       val p_disj : Wp.Lang.F.pred list -> Wp.Lang.F.pred       val p_any : ('-> Wp.Lang.F.pred) -> 'a list -> Wp.Lang.F.pred       val p_all : ('-> Wp.Lang.F.pred) -> 'a list -> Wp.Lang.F.pred       val p_call : Wp.Lang.lfun -> term list -> Wp.Lang.F.pred       val p_forall : var list -> Wp.Lang.F.pred -> Wp.Lang.F.pred       val p_exists : var list -> Wp.Lang.F.pred -> Wp.Lang.F.pred       val p_bind :         Qed.Logic.binder -> var -> Wp.Lang.F.pred -> Wp.Lang.F.pred       val e_subst : ?sigma:sigma -> (term -> term) -> term -> term       val p_subst :         ?sigma:sigma -> (term -> term) -> Wp.Lang.F.pred -> Wp.Lang.F.pred       val e_vars : term -> var list       val p_vars : Wp.Lang.F.pred -> var list       val p_close : Wp.Lang.F.pred -> Wp.Lang.F.pred       val idp : Wp.Lang.F.pred -> int       val varsp : Wp.Lang.F.pred -> Vars.t       val occurs : var -> term -> bool       val occursp : var -> Wp.Lang.F.pred -> bool       val intersect : term -> term -> bool       val intersectp : Wp.Lang.F.pred -> Wp.Lang.F.pred -> bool       val pp_tau : Format.formatter -> Wp.Lang.tau -> unit       val pp_var : Format.formatter -> var -> unit       val pp_vars : Format.formatter -> Vars.t -> unit       val pp_term : Format.formatter -> term -> unit       val pp_pred : Format.formatter -> Wp.Lang.F.pred -> unit       val debugp : Format.formatter -> Wp.Lang.F.pred -> unit       type env       val env : Vars.t -> Wp.Lang.F.env       val marker : Wp.Lang.F.env -> marks       val mark_e : marks -> term -> unit       val mark_p : marks -> Wp.Lang.F.pred -> unit       val define :         (Wp.Lang.F.env -> string -> term -> unit) ->         Wp.Lang.F.env -> marks -> Wp.Lang.F.env       val pp_eterm : Wp.Lang.F.env -> Format.formatter -> term -> unit       val pp_epred :         Wp.Lang.F.env -> Format.formatter -> Wp.Lang.F.pred -> unit       val pred : Wp.Lang.F.pred -> Wp.Lang.F.pred expression       val epred : Wp.Lang.F.pred -> term expression       val p_iter :         (Wp.Lang.F.pred -> unit) -> (term -> unit) -> Wp.Lang.F.pred -> unit       module Pmap :         sig           type key = pred           type 'a t           val is_empty : 'a t -> bool           val empty : 'a t           val add : key -> '-> 'a t -> 'a t           val mem : key -> 'a t -> bool           val find : key -> 'a t -> 'a           val remove : key -> 'a t -> 'a t           val compare : ('-> '-> int) -> 'a t -> 'a t -> int           val equal : ('-> '-> bool) -> 'a t -> 'a t -> bool           val iter : (key -> '-> unit) -> 'a t -> unit           val map : (key -> '-> 'b) -> 'a t -> 'b t           val mapf : (key -> '-> 'b option) -> 'a t -> 'b t           val mapq : (key -> '-> 'a option) -> 'a t -> 'a t           val filter : (key -> '-> bool) -> 'a t -> 'a t           val partition : (key -> '-> bool) -> 'a t -> 'a t * 'a t           val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b           val union : (key -> '-> '-> 'a) -> 'a t -> 'a t -> 'a t           val inter : (key -> '-> '-> 'c) -> 'a t -> 'b t -> 'c t           val interf : (key -> '-> '-> 'c option) -> 'a t -> 'b t -> 'c t           val interq : (key -> '-> '-> 'a option) -> 'a t -> 'a t -> 'a t           val diffq : (key -> '-> '-> 'a option) -> 'a t -> 'a t -> 'a t           val merge :             (key -> 'a option -> 'b option -> 'c option) ->             'a t -> 'b t -> 'c t           val insert : (key -> '-> '-> 'a) -> key -> '-> 'a t -> 'a t           val change :             (key -> '-> 'a option -> 'a option) ->             key -> '-> 'a t -> 'a t         end       module Pset :         sig           type elt = pred           type t           val empty : t           val is_empty : t -> bool           val mem : elt -> t -> bool           val find : elt -> t -> elt           val add : elt -> t -> t           val singleton : elt -> t           val remove : elt -> t -> t           val union : t -> t -> t           val inter : t -> t -> t           val diff : t -> t -> t           val compare : t -> t -> int           val equal : t -> t -> bool           val subset : t -> t -> bool           val iter : (elt -> unit) -> t -> unit           val fold : (elt -> '-> 'a) -> t -> '-> 'a           val for_all : (elt -> bool) -> t -> bool           val exists : (elt -> bool) -> t -> bool           val filter : (elt -> bool) -> t -> t           val partition : (elt -> bool) -> t -> t * t           val cardinal : t -> int           val elements : t -> elt list           val map : (elt -> elt) -> t -> t           val mapf : (elt -> elt option) -> t -> t           val intersect : t -> t -> bool         end       val release : unit -> unit       val set_builtin_1 : Wp.Lang.lfun -> (term -> term) -> unit       val set_builtin_2 : Wp.Lang.lfun -> (term -> term -> term) -> unit       val set_builtin_eqp :         Wp.Lang.lfun -> (term -> term -> Wp.Lang.F.pred) -> unit       module Check :         sig           val reset : unit -> unit           val set : string -> unit           val is_set : unit -> bool           val iter :             (qed:term -> raw:term -> goal:Wp.Lang.F.pred -> unit) -> unit         end     end   type gamma   val new_pool : ?copy:Wp.Lang.F.pool -> unit -> Wp.Lang.F.pool   val new_gamma : ?copy:Wp.Lang.gamma -> unit -> Wp.Lang.gamma   val local :     ?pool:Wp.Lang.F.pool -> ?gamma:Wp.Lang.gamma -> ('-> 'b) -> '-> 'b   val freshvar : ?basename:string -> Wp.Lang.F.tau -> Wp.Lang.F.var   val freshen : Wp.Lang.F.var -> Wp.Lang.F.var   val assume : Wp.Lang.F.pred -> unit   val without_assume : ('-> 'b) -> '-> 'b   val epsilon :     ?basename:string ->     Wp.Lang.F.tau -> (Wp.Lang.F.term -> Wp.Lang.F.pred) -> Wp.Lang.F.term   val hypotheses : Wp.Lang.gamma -> Wp.Lang.F.pred list   val variables : Wp.Lang.gamma -> Wp.Lang.F.var list   val get_pool : unit -> Wp.Lang.F.pool   val get_gamma : unit -> Wp.Lang.gamma   val get_hypotheses : unit -> Wp.Lang.F.pred list   val get_variables : unit -> Wp.Lang.F.var list   module Alpha :     sig       type t       val create : unit -> Wp.Lang.Alpha.t       val get : Wp.Lang.Alpha.t -> Wp.Lang.F.var -> Wp.Lang.F.var       val iter :         (Wp.Lang.F.var -> Wp.Lang.F.var -> unit) -> Wp.Lang.Alpha.t -> unit       val convert : Wp.Lang.Alpha.t -> Wp.Lang.F.term -> Wp.Lang.F.term       val convertp : Wp.Lang.Alpha.t -> Wp.Lang.F.pred -> Wp.Lang.F.pred     end end