sig
  type library = string
  type 'a infoprover = { altergo : 'a; why3 : 'a; coq : 'a; }
  val infoprover : '-> '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 Lang.mdt
    | Mrecord of Lang.mdt * Lang.fields
    | Atype of Cil_types.logic_type_info
    | Comp of Cil_types.compinfo
  and mdt = string Lang.extern
  and 'a extern = {
    ext_id : int;
    ext_link : 'Lang.infoprover;
    ext_library : Lang.library;
    ext_debug : string;
  }
  and fields = { mutable fields : Lang.field list; }
  and field =
      Mfield of Lang.mdt * Lang.fields * string * Lang.tau
    | Cfield of Cil_types.fieldinfo
  and tau = (Lang.field, Lang.adt) Qed.Logic.datatype
  type lfun =
      ACSL of Cil_types.logic_info
    | CTOR of Cil_types.logic_ctor_info
    | Model of Lang.model
  and model = {
    m_category : Lang.lfun Qed.Logic.category;
    m_params : Qed.Logic.sort list;
    m_resort : Qed.Logic.sort;
    m_result : Lang.tau option;
    m_source : Lang.source;
  }
  and source = Generated of string | Extern of Qed.Engine.link Lang.extern
  val builtin_type :
    name:string -> link:string Lang.infoprover -> library:string -> unit
  val datatype : library:string -> string -> Lang.adt
  val record :
    link:string Lang.infoprover ->
    library:string -> (string * Lang.tau) list -> Lang.adt
  val atype : Cil_types.logic_type_info -> Lang.adt
  val comp : Cil_types.compinfo -> Lang.adt
  val field : Lang.adt -> string -> Lang.field
  val fields_of_tau : Lang.tau -> Lang.field list
  val fields_of_field : Lang.field -> Lang.field list
  type balance = Nary | Left | Right
  val extern_s :
    library:Lang.library ->
    ?link:Qed.Engine.link Lang.infoprover ->
    ?category:Lang.lfun Qed.Logic.category ->
    ?params:Qed.Logic.sort list ->
    ?sort:Qed.Logic.sort -> ?result:Lang.tau -> string -> Lang.lfun
  val extern_f :
    library:Lang.library ->
    ?link:Qed.Engine.link Lang.infoprover ->
    ?balance:Lang.balance ->
    ?category:Lang.lfun Qed.Logic.category ->
    ?params:Qed.Logic.sort list ->
    ?sort:Qed.Logic.sort ->
    ?result:Lang.tau ->
    ('a, Format.formatter, unit, Lang.lfun) Pervasives.format4 -> 'a
  val extern_p :
    library:Lang.library ->
    ?bool:string ->
    ?prop:string ->
    ?link:Qed.Engine.link Lang.infoprover ->
    ?params:Qed.Logic.sort list -> unit -> Lang.lfun
  val extern_fp :
    library:Lang.library ->
    ?params:Qed.Logic.sort list ->
    ?link:string Lang.infoprover -> string -> Lang.lfun
  val generated_f :
    ?category:Lang.lfun Qed.Logic.category ->
    ?params:Qed.Logic.sort list ->
    ?sort:Qed.Logic.sort ->
    ?result:Lang.tau ->
    ('a, Format.formatter, unit, Lang.lfun) Pervasives.format4 -> 'a
  val generated_p : string -> Lang.lfun
  val tau_of_comp : Cil_types.compinfo -> Lang.tau
  val tau_of_object : Ctypes.c_object -> Lang.tau
  val tau_of_ctype : Cil_types.typ -> Lang.tau
  val tau_of_ltype : Cil_types.logic_type -> Lang.tau
  val tau_of_return : Cil_types.logic_info -> Lang.tau
  val tau_of_lfun : Lang.lfun -> Lang.tau
  val tau_of_field : Lang.field -> Lang.tau
  val tau_of_record : Lang.field -> Lang.tau
  val array : Lang.tau -> Lang.tau
  val farray : Lang.tau -> Lang.tau -> Lang.tau
  val pointer : (Cil_types.typ -> Lang.tau) Context.value
  val poly : string list Context.value
  val parameters : (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 : Lang.ADT.t -> string
      method datatypename : string -> string
      method field : Lang.Field.t -> string
      method fieldname : string -> string
      method funname : string -> string
      method virtual infoprover : 'Lang.infoprover -> 'a
      method link : 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 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 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 -> Lang.field -> term -> term
      val e_range : term -> term -> term
      val is_zero : term -> bool
      type pred
      type cmp = term -> term -> Lang.F.pred
      val p_true : Lang.F.pred
      val p_false : Lang.F.pred
      val p_equal : term -> term -> Lang.F.pred
      val p_neq : term -> term -> Lang.F.pred
      val p_leq : term -> term -> Lang.F.pred
      val p_lt : term -> term -> Lang.F.pred
      val p_positive : term -> Lang.F.pred
      val is_ptrue : Lang.F.pred -> Qed.Logic.maybe
      val is_pfalse : Lang.F.pred -> Qed.Logic.maybe
      val is_equal : term -> term -> Qed.Logic.maybe
      val eqp : Lang.F.pred -> Lang.F.pred -> bool
      val comparep : Lang.F.pred -> Lang.F.pred -> int
      val p_bool : term -> Lang.F.pred
      val e_prop : Lang.F.pred -> term
      val p_bools : term list -> Lang.F.pred list
      val e_props : Lang.F.pred list -> term list
      val lift : (term -> term) -> Lang.F.pred -> Lang.F.pred
      val p_not : Lang.F.pred -> Lang.F.pred
      val p_and : Lang.F.pred -> Lang.F.pred -> Lang.F.pred
      val p_or : Lang.F.pred -> Lang.F.pred -> Lang.F.pred
      val p_imply : Lang.F.pred -> Lang.F.pred -> Lang.F.pred
      val p_equiv : Lang.F.pred -> Lang.F.pred -> Lang.F.pred
      val p_hyps : Lang.F.pred list -> Lang.F.pred -> Lang.F.pred
      val p_if : Lang.F.pred -> Lang.F.pred -> Lang.F.pred -> Lang.F.pred
      val p_conj : Lang.F.pred list -> Lang.F.pred
      val p_disj : Lang.F.pred list -> Lang.F.pred
      val p_any : ('-> Lang.F.pred) -> 'a list -> Lang.F.pred
      val p_all : ('-> Lang.F.pred) -> 'a list -> Lang.F.pred
      val p_call : Lang.lfun -> term list -> Lang.F.pred
      val p_forall : var list -> Lang.F.pred -> Lang.F.pred
      val p_exists : var list -> Lang.F.pred -> Lang.F.pred
      val p_bind : Qed.Logic.binder -> var -> Lang.F.pred -> Lang.F.pred
      val e_subst : ?sigma:sigma -> (term -> term) -> term -> term
      val p_subst :
        ?sigma:sigma -> (term -> term) -> Lang.F.pred -> Lang.F.pred
      val p_close : Lang.F.pred -> Lang.F.pred
      val idp : Lang.F.pred -> int
      val varsp : Lang.F.pred -> Vars.t
      val occurs : var -> term -> bool
      val occursp : var -> Lang.F.pred -> bool
      val intersect : term -> term -> bool
      val intersectp : Lang.F.pred -> Lang.F.pred -> bool
      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 -> Lang.F.pred -> unit
      val debugp : Format.formatter -> Lang.F.pred -> unit
      type env
      val env : Vars.t -> Lang.F.env
      val marker : Lang.F.env -> marks
      val mark_e : marks -> term -> unit
      val mark_p : marks -> Lang.F.pred -> unit
      val define :
        (Lang.F.env -> string -> term -> unit) ->
        Lang.F.env -> marks -> Lang.F.env
      val pp_eterm : Lang.F.env -> Format.formatter -> term -> unit
      val pp_epred : Lang.F.env -> Format.formatter -> Lang.F.pred -> unit
      val pred : Lang.F.pred -> Lang.F.pred expression
      val epred : Lang.F.pred -> term expression
      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 : Lang.lfun -> (term -> term) -> unit
      val set_builtin_2 : Lang.lfun -> (term -> term -> term) -> unit
      val set_builtin_eqp :
        Lang.lfun -> (term -> term -> Lang.F.pred) -> unit
      val do_checks : bool Pervasives.ref
      val iter_checks :
        (qed:term -> raw:term -> goal:Lang.F.pred -> unit) -> unit
    end
  type gamma
  val new_pool : ?copy:Lang.F.pool -> unit -> Lang.F.pool
  val new_gamma : ?copy:Lang.gamma -> unit -> Lang.gamma
  val local :
    ?pool:Lang.F.pool -> ?gamma:Lang.gamma -> ('-> 'b) -> '-> 'b
  val freshvar : ?basename:string -> Lang.F.tau -> Lang.F.var
  val freshen : Lang.F.var -> Lang.F.var
  val assume : Lang.F.pred -> unit
  val without_assume : ('-> 'b) -> '-> 'b
  val epsilon :
    ?basename:string ->
    Lang.F.tau -> (Lang.F.term -> Lang.F.pred) -> Lang.F.term
  val hypotheses : Lang.gamma -> Lang.F.pred list
  val variables : Lang.gamma -> Lang.F.var list
  val get_pool : unit -> Lang.F.pool
  val get_gamma : unit -> Lang.gamma
  val get_hypotheses : unit -> Lang.F.pred list
  val get_variables : unit -> Lang.F.var list
  module Alpha :
    sig
      type t
      val create : unit -> Lang.Alpha.t
      val get : Lang.Alpha.t -> Lang.F.var -> Lang.F.var
      val iter : (Lang.F.var -> Lang.F.var -> unit) -> Lang.Alpha.t -> unit
      val convert : Lang.Alpha.t -> Lang.F.term -> Lang.F.term
      val convertp : Lang.Alpha.t -> Lang.F.pred -> Lang.F.pred
    end
end