sig
  type library = string
  val comp_id : Cil_types.compinfo -> string
  val comp_init_id : Cil_types.compinfo -> string
  val field_id : Cil_types.fieldinfo -> string
  val field_init_id : Cil_types.fieldinfo -> string
  val type_id : Cil_types.logic_type_info -> string
  val logic_id : Cil_types.logic_info -> string
  val ctor_id : Cil_types.logic_ctor_info -> string
  val lemma_id : string -> string
  type datakind = KValue | KInit
  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 * Lang.datakind
  and mdt = string Lang.extern
  and 'a extern = {
    ext_id : int;
    ext_link : 'a;
    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 * Lang.datakind
  and tau = (Lang.field, Lang.adt) Qed.Logic.datatype
  type t_builtin = E_mdt of Lang.mdt | E_poly of (Lang.tau list -> Lang.tau)
  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_result : Qed.Logic.sort;
    m_typeof : Lang.tau option list -> Lang.tau;
    m_source : Lang.source;
    m_coloring : bool;
  }
  and source =
      Generated of WpContext.context option * string
    | Extern of Qed.Engine.link Lang.extern
  val mem_builtin_type : name:string -> bool
  val is_builtin : Cil_types.logic_type_info -> bool
  val is_builtin_type : name:string -> Lang.tau -> bool
  val get_builtin_type : name:string -> Lang.adt
  val datatype : library:string -> string -> Lang.adt
  val record :
    link:string -> library:string -> (string * Lang.tau) list -> Lang.adt
  val comp : Cil_types.compinfo -> Lang.adt
  val comp_init : Cil_types.compinfo -> Lang.adt
  val field : Lang.adt -> string -> Lang.field
  val fields_of_adt : Lang.adt -> Lang.field list
  val fields_of_tau : Lang.tau -> Lang.field list
  val fields_of_field : Lang.field -> Lang.field list
  val atype : Cil_types.logic_type_info -> Lang.tau list -> Lang.tau
  val adt : Cil_types.logic_type_info -> Lang.adt
  type balance = Nary | Left | Right
  val extern_s :
    library:Lang.library ->
    ?link:Qed.Engine.link ->
    ?category:Lang.lfun Qed.Logic.category ->
    ?params:Qed.Logic.sort list ->
    ?sort:Qed.Logic.sort ->
    ?result:Lang.tau ->
    ?coloring:bool ->
    ?typecheck:(Lang.tau option list -> Lang.tau) -> string -> Lang.lfun
  val extern_f :
    library:Lang.library ->
    ?link:Qed.Engine.link ->
    ?balance:Lang.balance ->
    ?category:Lang.lfun Qed.Logic.category ->
    ?params:Qed.Logic.sort list ->
    ?sort:Qed.Logic.sort ->
    ?result:Lang.tau ->
    ?coloring:bool ->
    ?typecheck:(Lang.tau option list -> Lang.tau) ->
    ('a, Stdlib.Format.formatter, unit, Lang.lfun) Stdlib.format4 -> 'a
  val extern_p :
    library:Lang.library ->
    ?bool:string ->
    ?prop:string ->
    ?link:Qed.Engine.link ->
    ?params:Qed.Logic.sort list -> ?coloring:bool -> unit -> Lang.lfun
  val extern_fp :
    library:Lang.library ->
    ?params:Qed.Logic.sort list ->
    ?link:string -> ?coloring:bool -> string -> Lang.lfun
  val generated_f :
    ?context:bool ->
    ?category:Lang.lfun Qed.Logic.category ->
    ?params:Qed.Logic.sort list ->
    ?sort:Qed.Logic.sort ->
    ?result:Lang.tau ->
    ?coloring:bool ->
    ('a, Stdlib.Format.formatter, unit, Lang.lfun) Stdlib.format4 -> 'a
  val generated_p : ?context:bool -> ?coloring:bool -> string -> Lang.lfun
  val extern_t : string -> link:string -> library:Lang.library -> Lang.mdt
  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 option list -> Lang.tau
  val tau_of_field : Lang.field -> Lang.tau
  val tau_of_record : Lang.field -> Lang.tau
  val init_of_object : Ctypes.c_object -> Lang.tau
  val init_of_ctype : Cil_types.typ -> Lang.tau
  val t_int : Lang.tau
  val t_real : Lang.tau
  val t_bool : Lang.tau
  val t_prop : Lang.tau
  val t_addr : unit -> Lang.tau
  val t_comp : Cil_types.compinfo -> Lang.tau
  val t_init : Cil_types.compinfo -> Lang.tau
  val t_float : Ctypes.c_float -> Lang.tau
  val t_array : Lang.tau -> Lang.tau
  val t_farray : Lang.tau -> Lang.tau -> Lang.tau
  val t_datatype : Lang.adt -> Lang.tau list -> Lang.tau
  val t_matrix : Lang.tau -> int -> Lang.tau
  val pointer : Lang.tau Context.value
  val floats : (Ctypes.c_float -> Lang.tau) Context.value
  val poly : string list Context.value
  val builtin_types : (string -> Lang.t_builtin) Context.value
  val parameters : (Lang.lfun -> Qed.Logic.sort list) -> unit
  val name_of_lfun : Lang.lfun -> string
  val name_of_field : Lang.field -> string
  val is_coloring_lfun : Lang.lfun -> bool
  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 datatype : Lang.ADT.t -> string
      method field : Lang.Field.t -> string
      method link : Lang.Fun.t -> Qed.Engine.link
      method virtual sanitize : string -> string
      method sanitize_field : string -> string
      method sanitize_fun : string -> string
      method sanitize_type : string -> string
    end
  module F :
    sig
      module QED :
        sig
          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 lc_term
          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 iter2 :
                (key -> 'a option -> 'b option -> unit) ->
                'a t -> 'b t -> unit
              val subset : (key -> '-> '-> bool) -> 'a t -> 'b t -> bool
              val insert :
                (key -> '-> '-> 'a) -> key -> '-> 'a t -> 'a t
              val change :
                (key -> '-> 'a option -> 'a option) ->
                key -> '-> 'a t -> 'a t
            end
          module STset :
            sig
              type elt = term
              type t
              val empty : t
              val is_empty : t -> bool
              val mem : elt -> t -> bool
              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 disjoint : t -> t -> bool
              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 map : (elt -> elt) -> t -> t
              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 filter_map : (elt -> elt option) -> t -> t
              val partition : (elt -> bool) -> t -> t * t
              val cardinal : t -> int
              val elements : t -> elt list
              val min_elt : t -> elt
              val min_elt_opt : t -> elt option
              val max_elt : t -> elt
              val max_elt_opt : t -> elt option
              val choose : t -> elt
              val choose_opt : t -> elt option
              val split : elt -> t -> t * bool * t
              val find : elt -> t -> elt
              val find_opt : elt -> t -> elt option
              val find_first : (elt -> bool) -> t -> elt
              val find_first_opt : (elt -> bool) -> t -> elt option
              val find_last : (elt -> bool) -> t -> elt
              val find_last_opt : (elt -> bool) -> t -> elt option
              val of_list : elt list -> t
              val to_seq_from : elt -> t -> elt Seq.t
              val to_seq : t -> elt Seq.t
              val to_rev_seq : t -> elt Seq.t
              val add_seq : elt Seq.t -> t -> t
              val of_seq : elt Seq.t -> t
            end
          module STmap :
            sig
              type key = term
              type +!'a t
              val empty : 'a t
              val is_empty : 'a t -> bool
              val mem : key -> 'a t -> bool
              val add : key -> '-> 'a t -> 'a t
              val update : key -> ('a option -> 'a option) -> 'a t -> 'a t
              val singleton : key -> '-> 'a t
              val remove : key -> 'a t -> 'a t
              val merge :
                (key -> 'a option -> 'b option -> 'c option) ->
                'a t -> 'b t -> 'c t
              val union :
                (key -> '-> '-> 'a option) -> 'a t -> '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 fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
              val for_all : (key -> '-> bool) -> 'a t -> bool
              val exists : (key -> '-> bool) -> 'a t -> bool
              val filter : (key -> '-> bool) -> 'a t -> 'a t
              val filter_map : (key -> '-> 'b option) -> 'a t -> 'b t
              val partition : (key -> '-> bool) -> 'a t -> 'a t * 'a t
              val cardinal : 'a t -> int
              val bindings : 'a t -> (key * 'a) list
              val min_binding : 'a t -> key * 'a
              val min_binding_opt : 'a t -> (key * 'a) option
              val max_binding : 'a t -> key * 'a
              val max_binding_opt : 'a t -> (key * 'a) option
              val choose : 'a t -> key * 'a
              val choose_opt : 'a t -> (key * 'a) option
              val split : key -> 'a t -> 'a t * 'a option * 'a t
              val find : key -> 'a t -> 'a
              val find_opt : key -> 'a t -> 'a option
              val find_first : (key -> bool) -> 'a t -> key * 'a
              val find_first_opt : (key -> bool) -> 'a t -> (key * 'a) option
              val find_last : (key -> bool) -> 'a t -> key * 'a
              val find_last_opt : (key -> bool) -> 'a t -> (key * 'a) option
              val map : ('-> 'b) -> 'a t -> 'b t
              val mapi : (key -> '-> 'b) -> 'a t -> 'b t
              val to_seq : 'a t -> (key * 'a) Seq.t
              val to_rev_seq : 'a t -> (key * 'a) Seq.t
              val to_seq_from : key -> 'a t -> (key * 'a) Seq.t
              val add_seq : (key * 'a) Seq.t -> 'a t -> 'a t
              val of_seq : (key * 'a) Seq.t -> 'a t
            end
          type var = Var.t
          type tau = (Field.t, ADT.t) Qed.Logic.datatype
          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 iter2 :
                (key -> 'a option -> 'b option -> unit) ->
                'a t -> 'b t -> unit
              val subset : (key -> '-> '-> bool) -> 'a t -> 'b t -> bool
              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 =
              (Field.t, ADT.t, Fun.t, var, lc_term, 'a) Qed.Logic.term_repr
          type repr = term expression
          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
          type path = int list
          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_float : float -> term
          val e_zint : Z.t -> term
          val e_real : Q.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_const : tau -> 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 : ?result:tau -> Fun.t -> term list -> term
          val e_repr : ?result:tau -> 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_apply : term -> term list -> term
          val e_bind : Qed.Logic.binder -> var -> term -> term
          val lc_open : var -> lc_term -> term
          val e_unbind : var -> lc_term -> term
          val e_open :
            pool:pool ->
            ?forall:bool ->
            ?exists:bool ->
            ?lambda:bool -> term -> (Qed.Logic.binder * var) list * term
          val e_close : (Qed.Logic.binder * var) list -> term -> term
          type sigma
          val sigma : ?pool:pool -> unit -> sigma
          module Subst :
            sig
              type t = sigma
              val create : ?pool:pool -> unit -> t
              val copy : sigma -> sigma
              val fresh : t -> tau -> var
              val find : t -> term -> term
              val filter : t -> term -> bool
              val add : t -> term -> term -> unit
              val add_fun : t -> (term -> term) -> unit
              val add_filter : t -> (term -> bool) -> unit
              val add_var : t -> var -> unit
              val add_vars : t -> Vars.t -> unit
              val add_term : t -> term -> unit
            end
          val e_subst : sigma -> term -> term
          val e_subst_var : var -> term -> term -> term
          val lc_vars : term -> Qed.Bvars.t
          val lc_closed : term -> bool
          val lc_repr : lc_term -> term
          val lc_iter : (term -> unit) -> term -> unit
          val f_map :
            ?pool:pool ->
            ?forall:bool ->
            ?exists:bool -> ?lambda:bool -> (term -> term) -> term -> term
          val f_iter :
            ?pool:pool ->
            ?forall:bool ->
            ?exists:bool -> ?lambda:bool -> (term -> unit) -> term -> unit
          val typeof :
            ?field:(Field.t -> tau) ->
            ?record:(Field.t -> tau) ->
            ?call:(Fun.t -> tau option list -> tau) -> term -> tau
          val set_builtin :
            ?force:bool -> Fun.t -> (term list -> term) -> unit
          val set_builtin' :
            ?force:bool -> Fun.t -> (term list -> tau option -> term) -> unit
          val set_builtin_map :
            ?force:bool -> Fun.t -> (term list -> term list) -> unit
          val set_builtin_get :
            ?force:bool ->
            Fun.t -> (term list -> tau option -> term -> term) -> unit
          val set_builtin_eq :
            ?force:bool -> Fun.t -> (term -> term -> term) -> unit
          val set_builtin_leq :
            ?force:bool -> Fun.t -> (term -> term -> term) -> unit
          val consequence : term -> term -> term
          val literal : term -> bool * term
          val affine : term -> 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
          val is_subterm : term -> term -> bool
          val shared :
            ?shared:(term -> bool) ->
            ?shareable:(term -> bool) ->
            ?subterms:((term -> unit) -> term -> unit) ->
            term list -> term list
          type marks
          val marks :
            ?shared:(term -> bool) ->
            ?shareable:(term -> bool) ->
            ?subterms:((term -> unit) -> term -> unit) -> unit -> marks
          val mark : marks -> term -> unit
          val share : marks -> term -> unit
          val defs : marks -> term list
        end
      type var = Lang.F.QED.var
      type tau = Lang.F.QED.tau
      type pool = Lang.F.QED.pool
      module Tau = QED.Tau
      module Var = QED.Var
      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 iter2 :
            (key -> 'a option -> 'b option -> unit) -> 'a t -> 'b t -> unit
          val subset : (key -> '-> '-> bool) -> 'a t -> 'b t -> bool
          val insert : (key -> '-> '-> 'a) -> key -> '-> 'a t -> 'a t
          val change :
            (key -> '-> 'a option -> 'a option) ->
            key -> '-> 'a t -> 'a t
        end
      val pool : ?copy:Lang.F.pool -> unit -> Lang.F.pool
      val fresh : Lang.F.pool -> ?basename:string -> Lang.F.tau -> Lang.F.var
      val alpha : Lang.F.pool -> Lang.F.var -> Lang.F.var
      val add_var : Lang.F.pool -> Lang.F.var -> unit
      val add_vars : Lang.F.pool -> Lang.F.Vars.t -> unit
      val tau_of_var : Lang.F.var -> Lang.F.tau
      type term = Lang.F.QED.term
      type record = (Lang.field * Lang.F.term) list
      val hash : Lang.F.term -> int
      val equal : Lang.F.term -> Lang.F.term -> bool
      val compare : Lang.F.term -> Lang.F.term -> int
      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 iter2 :
            (key -> 'a option -> 'b option -> unit) -> 'a t -> 'b t -> unit
          val subset : (key -> '-> '-> bool) -> 'a t -> 'b t -> bool
          val insert : (key -> '-> '-> 'a) -> key -> '-> 'a t -> 'a t
          val change :
            (key -> '-> 'a option -> 'a option) ->
            key -> '-> 'a t -> 'a t
        end
      type unop = Lang.F.term -> Lang.F.term
      type binop = Lang.F.term -> Lang.F.term -> Lang.F.term
      val e_zero : Lang.F.term
      val e_one : Lang.F.term
      val e_minus_one : Lang.F.term
      val e_minus_one_real : Lang.F.term
      val e_one_real : Lang.F.term
      val e_zero_real : Lang.F.term
      val constant : Lang.F.term -> Lang.F.term
      val e_fact : int -> Lang.F.term -> Lang.F.term
      val e_int64 : int64 -> Lang.F.term
      val e_bigint : Integer.t -> Lang.F.term
      val e_float : float -> Lang.F.term
      val e_setfield :
        Lang.F.term -> Lang.field -> Lang.F.term -> Lang.F.term
      val e_range : Lang.F.term -> Lang.F.term -> Lang.F.term
      val is_zero : Lang.F.term -> bool
      val e_true : Lang.F.term
      val e_false : Lang.F.term
      val e_bool : bool -> Lang.F.term
      val e_literal : bool -> Lang.F.term -> Lang.F.term
      val e_int : int -> Lang.F.term
      val e_zint : Z.t -> Lang.F.term
      val e_real : Q.t -> Lang.F.term
      val e_var : Lang.F.var -> Lang.F.term
      val e_opp : Lang.F.term -> Lang.F.term
      val e_times : Z.t -> Lang.F.term -> Lang.F.term
      val e_sum : Lang.F.term list -> Lang.F.term
      val e_prod : Lang.F.term list -> Lang.F.term
      val e_add : Lang.F.term -> Lang.F.term -> Lang.F.term
      val e_sub : Lang.F.term -> Lang.F.term -> Lang.F.term
      val e_mul : Lang.F.term -> Lang.F.term -> Lang.F.term
      val e_div : Lang.F.term -> Lang.F.term -> Lang.F.term
      val e_mod : Lang.F.term -> Lang.F.term -> Lang.F.term
      val e_eq : Lang.F.term -> Lang.F.term -> Lang.F.term
      val e_neq : Lang.F.term -> Lang.F.term -> Lang.F.term
      val e_leq : Lang.F.term -> Lang.F.term -> Lang.F.term
      val e_lt : Lang.F.term -> Lang.F.term -> Lang.F.term
      val e_imply : Lang.F.term list -> Lang.F.term -> Lang.F.term
      val e_equiv : Lang.F.term -> Lang.F.term -> Lang.F.term
      val e_and : Lang.F.term list -> Lang.F.term
      val e_or : Lang.F.term list -> Lang.F.term
      val e_not : Lang.F.term -> Lang.F.term
      val e_if : Lang.F.term -> Lang.F.term -> Lang.F.term -> Lang.F.term
      val e_const : Lang.F.tau -> Lang.F.term -> Lang.F.term
      val e_get : Lang.F.term -> Lang.F.term -> Lang.F.term
      val e_set : Lang.F.term -> Lang.F.term -> Lang.F.term -> Lang.F.term
      val e_getfield : Lang.F.term -> Lang.Field.t -> Lang.F.term
      val e_record : Lang.F.record -> Lang.F.term
      val e_fun :
        ?result:Lang.F.tau -> Lang.Fun.t -> Lang.F.term list -> Lang.F.term
      val e_bind :
        Qed.Logic.binder -> Lang.F.var -> Lang.F.term -> Lang.F.term
      val e_open :
        pool:Lang.F.pool ->
        ?forall:bool ->
        ?exists:bool ->
        ?lambda:bool ->
        Lang.F.term -> (Qed.Logic.binder * Lang.F.var) list * Lang.F.term
      val e_close :
        (Qed.Logic.binder * Lang.F.var) list -> Lang.F.term -> Lang.F.term
      type pred
      type cmp = Lang.F.term -> Lang.F.term -> Lang.F.pred
      type operator = Lang.F.pred -> Lang.F.pred -> Lang.F.pred
      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 iter2 :
            (key -> 'a option -> 'b option -> unit) -> 'a t -> 'b t -> unit
          val subset : (key -> '-> '-> bool) -> 'a t -> 'b t -> bool
          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 p_true : Lang.F.pred
      val p_false : Lang.F.pred
      val p_equal : Lang.F.term -> Lang.F.term -> Lang.F.pred
      val p_equals : (Lang.F.term * Lang.F.term) list -> Lang.F.pred list
      val p_neq : Lang.F.term -> Lang.F.term -> Lang.F.pred
      val p_leq : Lang.F.term -> Lang.F.term -> Lang.F.pred
      val p_lt : Lang.F.term -> Lang.F.term -> Lang.F.pred
      val p_positive : Lang.F.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 : Lang.F.term -> Lang.F.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 : Lang.F.term -> Lang.F.pred
      val e_prop : Lang.F.pred -> Lang.F.term
      val p_bools : Lang.F.term list -> Lang.F.pred list
      val e_props : Lang.F.pred list -> Lang.F.term list
      val e_lift : (Lang.F.term -> Lang.F.term) -> Lang.F.pred -> Lang.F.pred
      val p_lift : (Lang.F.pred -> Lang.F.pred) -> Lang.F.term -> Lang.F.term
      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 -> Lang.F.term list -> Lang.F.pred
      val p_forall : Lang.F.var list -> Lang.F.pred -> Lang.F.pred
      val p_exists : Lang.F.var list -> Lang.F.pred -> Lang.F.pred
      val p_bind :
        Qed.Logic.binder -> Lang.F.var -> Lang.F.pred -> Lang.F.pred
      type sigma
      module Subst :
        sig
          val copy : Lang.F.sigma -> Lang.F.sigma
          val find : Lang.F.sigma -> Lang.F.term -> Lang.F.term
          val add : Lang.F.sigma -> Lang.F.term -> Lang.F.term -> unit
          val add_fun : Lang.F.sigma -> (Lang.F.term -> Lang.F.term) -> unit
          val add_filter : Lang.F.sigma -> (Lang.F.term -> bool) -> unit
        end
      val e_subst : Lang.F.sigma -> Lang.F.term -> Lang.F.term
      val p_subst : Lang.F.sigma -> Lang.F.pred -> Lang.F.pred
      val p_subst_var :
        Lang.F.var -> Lang.F.term -> Lang.F.pred -> Lang.F.pred
      val e_vars : Lang.F.term -> Lang.F.var list
      val p_vars : Lang.F.pred -> Lang.F.var list
      val p_close : Lang.F.pred -> Lang.F.pred
      val pp_tau : Stdlib.Format.formatter -> Lang.F.tau -> unit
      val pp_var : Stdlib.Format.formatter -> Lang.F.var -> unit
      val pp_vars : Stdlib.Format.formatter -> Lang.F.Vars.t -> unit
      val pp_term : Stdlib.Format.formatter -> Lang.F.term -> unit
      val pp_pred : Stdlib.Format.formatter -> Lang.F.pred -> unit
      val debugp : Stdlib.Format.formatter -> Lang.F.pred -> unit
      type env
      val context_pp : Lang.F.env Context.value
      type marks = Lang.F.QED.marks
      val env : Lang.F.Vars.t -> Lang.F.env
      val marker : Lang.F.env -> Lang.F.marks
      val mark_e : Lang.F.marks -> Lang.F.term -> unit
      val mark_p : Lang.F.marks -> Lang.F.pred -> unit
      val defs : Lang.F.marks -> Lang.F.term list
      val define :
        (Lang.F.env -> string -> Lang.F.term -> unit) ->
        Lang.F.env -> Lang.F.marks -> Lang.F.env
      val pp_eterm :
        Lang.F.env -> Stdlib.Format.formatter -> Lang.F.term -> unit
      val pp_epred :
        Lang.F.env -> Stdlib.Format.formatter -> Lang.F.pred -> unit
      val p_expr : Lang.F.pred -> Lang.F.pred Lang.F.QED.expression
      val e_expr : Lang.F.pred -> Lang.F.term Lang.F.QED.expression
      val lc_closed : Lang.F.term -> bool
      val lc_iter : (Lang.F.term -> unit) -> Lang.F.term -> unit
      val decide : Lang.F.term -> bool
      val basename : Lang.F.term -> string
      val is_true : Lang.F.term -> Qed.Logic.maybe
      val is_false : Lang.F.term -> Qed.Logic.maybe
      val is_prop : Lang.F.term -> bool
      val is_int : Lang.F.term -> bool
      val is_real : Lang.F.term -> bool
      val is_arith : Lang.F.term -> bool
      val is_closed : Lang.F.term -> bool
      val is_simple : Lang.F.term -> bool
      val is_atomic : Lang.F.term -> bool
      val is_primitive : Lang.F.term -> bool
      val is_neutral : Lang.Fun.t -> Lang.F.term -> bool
      val is_absorbant : Lang.Fun.t -> Lang.F.term -> bool
      val record_with : Lang.F.record -> (Lang.F.term * Lang.F.record) option
      val are_equal : Lang.F.term -> Lang.F.term -> Qed.Logic.maybe
      val eval_eq : Lang.F.term -> Lang.F.term -> bool
      val eval_neq : Lang.F.term -> Lang.F.term -> bool
      val eval_lt : Lang.F.term -> Lang.F.term -> bool
      val eval_leq : Lang.F.term -> Lang.F.term -> bool
      val repr : Lang.F.term -> Lang.F.QED.repr
      val sort : Lang.F.term -> Qed.Logic.sort
      val vars : Lang.F.term -> Lang.F.Vars.t
      val varsp : Lang.F.pred -> Lang.F.Vars.t
      val occurs : Lang.F.var -> Lang.F.term -> bool
      val occursp : Lang.F.var -> Lang.F.pred -> bool
      val intersect : Lang.F.term -> Lang.F.term -> bool
      val intersectp : Lang.F.pred -> Lang.F.pred -> bool
      val is_subterm : Lang.F.term -> Lang.F.term -> bool
      val typeof :
        ?field:(Lang.Field.t -> Lang.F.tau) ->
        ?record:(Lang.Field.t -> Lang.F.tau) ->
        ?call:(Lang.Fun.t -> Lang.F.tau option list -> Lang.F.tau) ->
        Lang.F.term -> Lang.F.tau
      val set_builtin :
        Lang.lfun -> (Lang.F.term list -> Lang.F.term) -> unit
      val set_builtin_get :
        Lang.lfun ->
        (Lang.F.term list -> Lang.F.tau option -> Lang.F.term -> Lang.F.term) ->
        unit
      val set_builtin_1 : Lang.lfun -> Lang.F.unop -> unit
      val set_builtin_2 : Lang.lfun -> Lang.F.binop -> unit
      val set_builtin_2' :
        Lang.lfun ->
        (Lang.F.term -> Lang.F.term -> Lang.F.tau option -> Lang.F.term) ->
        unit
      val set_builtin_eq : Lang.lfun -> Lang.F.binop -> unit
      val set_builtin_leq : Lang.lfun -> Lang.F.binop -> unit
      val set_builtin_eqp : Lang.lfun -> Lang.F.cmp -> unit
      val release : unit -> unit
    end
  module N :
    sig
      val ( + ) : Lang.F.binop
      val ( - ) : Lang.F.binop
      val ( ~- ) : Lang.F.unop
      val ( * ) : Lang.F.binop
      val ( / ) : Lang.F.binop
      val ( mod ) : Lang.F.binop
      val ( = ) : Lang.F.cmp
      val ( < ) : Lang.F.cmp
      val ( > ) : Lang.F.cmp
      val ( <= ) : Lang.F.cmp
      val ( >= ) : Lang.F.cmp
      val ( <> ) : Lang.F.cmp
      val ( ==> ) : Lang.F.operator
      val ( && ) : Lang.F.operator
      val ( || ) : Lang.F.operator
      val not : Lang.F.pred -> Lang.F.pred
      val ( $ ) :
        ?result:Lang.tau -> Lang.lfun -> Lang.F.term list -> Lang.F.term
      val ( $$ ) : Lang.lfun -> Lang.F.term list -> Lang.F.pred
    end
  type gamma
  val new_pool :
    ?copy:Lang.F.pool -> ?vars:Lang.F.Vars.t -> unit -> Lang.F.pool
  val new_gamma : ?copy:Lang.gamma -> unit -> Lang.gamma
  val local :
    ?pool:Lang.F.pool ->
    ?vars:Lang.F.Vars.t -> ?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 hypotheses : Lang.gamma -> Lang.F.pred list
  val get_pool : unit -> Lang.F.pool
  val get_gamma : unit -> Lang.gamma
  val has_gamma : unit -> bool
  val get_hypotheses : unit -> Lang.F.pred list
  val filter_hypotheses : Lang.F.var list -> Lang.F.pred list
  val sigma : unit -> Lang.F.sigma
  val alpha : unit -> Lang.F.sigma
  val subst : Lang.F.var list -> Lang.F.term list -> Lang.F.sigma
  val e_subst : (Lang.F.term -> Lang.F.term) -> Lang.F.term -> Lang.F.term
  val p_subst : (Lang.F.term -> Lang.F.term) -> Lang.F.pred -> Lang.F.pred
  exception Contradiction
  val is_literal : Lang.F.term -> bool
  val iter_consequence_literals :
    (Lang.F.term -> unit) -> Lang.F.term -> unit
  class type simplifier =
    object
      method assume : Lang.F.pred -> unit
      method copy : Lang.simplifier
      method equivalent_branch : Lang.F.pred -> Lang.F.pred
      method equivalent_exp : Lang.F.term -> Lang.F.term
      method fixpoint : unit
      method infer : Lang.F.pred list
      method name : string
      method stronger_goal : Lang.F.pred -> Lang.F.pred
      method target : Lang.F.pred -> unit
      method weaker_hyp : Lang.F.pred -> Lang.F.pred
    end
  module For_export :
    sig
      type specific_equality = {
        for_tau : Lang.F.tau -> bool;
        mk_new_eq : Lang.F.binop;
      }
      val rebuild :
        ?cache:Lang.F.term Lang.F.Tmap.t ->
        Lang.F.term -> Lang.F.term * Lang.F.term Lang.F.Tmap.t
      val set_builtin :
        Lang.Fun.t -> (Lang.F.term list -> Lang.F.term) -> unit
      val set_builtin' :
        Lang.Fun.t ->
        (Lang.F.term list -> Lang.F.tau option -> Lang.F.term) -> unit
      val set_builtin_eq :
        Lang.Fun.t -> (Lang.F.term -> Lang.F.term -> Lang.F.term) -> unit
      val set_builtin_leq :
        Lang.Fun.t -> (Lang.F.term -> Lang.F.term -> Lang.F.term) -> unit
      val in_state : ('-> 'b) -> '-> 'b
    end
end