functor (C : Exp_context) ->
  sig
    val exp_subst :
      Types.t Types.TNfmap.t * Typed_ast.exp_subst Typed_ast.Nfmap.t ->
      Typed_ast.exp -> Typed_ast.exp
    val push_subst :
      Types.t Types.TNfmap.t * Typed_ast.exp_subst Typed_ast.Nfmap.t ->
      Typed_ast.pat list ->
      Typed_ast.exp -> Typed_ast.pat list * Typed_ast.exp
    val exp_to_term : Typed_ast.exp -> Typed_ast.exp_aux
    val exp_to_free : Typed_ast.exp -> Types.t Typed_ast.Nfmap.t
    val type_eq : Ast.l -> string -> Types.t -> Types.t -> unit
    val mk_lnumeral :
      Ast.l -> Typed_ast.lskips -> int -> Types.t option -> Typed_ast.lit
    val mk_lnum :
      Ast.l -> Typed_ast.lskips -> int -> Types.t -> Typed_ast.lit
    val mk_lbool :
      Ast.l -> Typed_ast.lskips -> bool -> Types.t option -> Typed_ast.lit
    val mk_lbit :
      Ast.l -> Typed_ast.lskips -> int -> Types.t option -> Typed_ast.lit
    val mk_lundef :
      Ast.l -> Typed_ast.lskips -> string -> Types.t -> Typed_ast.lit
    val mk_lstring :
      Ast.l -> Typed_ast.lskips -> string -> Types.t option -> Typed_ast.lit
    val mk_twild : Ast.l -> Typed_ast.lskips -> Types.t -> Types.src_t
    val mk_tvar :
      Ast.l -> Typed_ast.lskips -> Tyvar.t -> Types.t -> Types.src_t
    val mk_tfn :
      Ast.l ->
      Types.src_t ->
      Typed_ast.lskips -> Types.src_t -> Types.t option -> Types.src_t
    val mk_ttup :
      Ast.l ->
      Types.src_t Typed_ast.lskips_seplist -> Types.t option -> Types.src_t
    val mk_tapp :
      Ast.l ->
      Path.t Types.id -> Types.src_t list -> Types.t option -> Types.src_t
    val mk_tparen :
      Ast.l ->
      Typed_ast.lskips ->
      Types.src_t -> Typed_ast.lskips -> Types.t option -> Types.src_t
    val mk_pwild : Ast.l -> Typed_ast.lskips -> Types.t -> Typed_ast.pat
    val mk_pas :
      Ast.l ->
      Typed_ast.lskips ->
      Typed_ast.pat ->
      Typed_ast.lskips ->
      Typed_ast.name_l -> Typed_ast.lskips -> Types.t option -> Typed_ast.pat
    val mk_ptyp :
      Ast.l ->
      Typed_ast.lskips ->
      Typed_ast.pat ->
      Typed_ast.lskips ->
      Types.src_t -> Typed_ast.lskips -> Types.t option -> Typed_ast.pat
    val mk_pvar : Ast.l -> Name.lskips_t -> Types.t -> Typed_ast.pat
    val mk_pconst :
      Ast.l ->
      Typed_ast.const_descr_ref Types.id ->
      Typed_ast.pat list -> Types.t option -> Typed_ast.pat
    val mk_pbackend :
      Ast.l ->
      Typed_ast.lskips ->
      Ident.t ->
      Types.t -> Typed_ast.pat list -> Types.t option -> Typed_ast.pat
    val mk_precord :
      Ast.l ->
      Typed_ast.lskips ->
      (Typed_ast.const_descr_ref Types.id * Typed_ast.lskips * Typed_ast.pat)
      Typed_ast.lskips_seplist ->
      Typed_ast.lskips -> Types.t option -> Typed_ast.pat
    val mk_ptup :
      Ast.l ->
      Typed_ast.lskips ->
      Typed_ast.pat Typed_ast.lskips_seplist ->
      Typed_ast.lskips -> Types.t option -> Typed_ast.pat
    val mk_plist :
      Ast.l ->
      Typed_ast.lskips ->
      Typed_ast.pat Typed_ast.lskips_seplist ->
      Typed_ast.lskips -> Types.t -> Typed_ast.pat
    val mk_pvector :
      Ast.l ->
      Typed_ast.lskips ->
      Typed_ast.pat Typed_ast.lskips_seplist ->
      Typed_ast.lskips -> Types.t -> Typed_ast.pat
    val mk_pvectorc :
      Ast.l ->
      Typed_ast.lskips ->
      Typed_ast.pat list -> Typed_ast.lskips -> Types.t -> Typed_ast.pat
    val mk_pparen :
      Ast.l ->
      Typed_ast.lskips ->
      Typed_ast.pat -> Typed_ast.lskips -> Types.t option -> Typed_ast.pat
    val mk_pcons :
      Ast.l ->
      Typed_ast.pat ->
      Typed_ast.lskips -> Typed_ast.pat -> Types.t option -> Typed_ast.pat
    val mk_pnum_add :
      Ast.l ->
      Typed_ast.name_l ->
      Typed_ast.lskips ->
      Typed_ast.lskips -> int -> Types.t option -> Typed_ast.pat
    val mk_plit : Ast.l -> Typed_ast.lit -> Types.t option -> Typed_ast.pat
    val mk_pvar_annot :
      Ast.l ->
      Name.lskips_t -> Types.src_t -> Types.t option -> Typed_ast.pat
    val mk_var : Ast.l -> Name.lskips_t -> Types.t -> Typed_ast.exp
    val mk_nvar_e :
      Ast.l -> Typed_ast.lskips -> Nvar.t -> Types.t -> Typed_ast.exp
    val mk_backend :
      Ast.l -> Typed_ast.lskips -> Ident.t -> Types.t -> Typed_ast.exp
    val mk_const :
      Ast.l ->
      Typed_ast.const_descr_ref Types.id -> Types.t option -> Typed_ast.exp
    val mk_fun :
      Ast.l ->
      Typed_ast.lskips ->
      Typed_ast.pat list ->
      Typed_ast.lskips -> Typed_ast.exp -> Types.t option -> Typed_ast.exp
    val mk_function :
      Ast.l ->
      Typed_ast.lskips ->
      (Typed_ast.pat * Typed_ast.lskips * Typed_ast.exp * Ast.l)
      Typed_ast.lskips_seplist ->
      Typed_ast.lskips -> Types.t option -> Typed_ast.exp
    val mk_app :
      Ast.l ->
      Typed_ast.exp -> Typed_ast.exp -> Types.t option -> Typed_ast.exp
    val mk_infix :
      Ast.l ->
      Typed_ast.exp ->
      Typed_ast.exp -> Typed_ast.exp -> Types.t option -> Typed_ast.exp
    val mk_record :
      Ast.l ->
      Typed_ast.lskips ->
      (Typed_ast.const_descr_ref Types.id * Typed_ast.lskips *
       Typed_ast.exp * Ast.l)
      Typed_ast.lskips_seplist ->
      Typed_ast.lskips -> Types.t option -> Typed_ast.exp
    val mk_recup :
      Ast.l ->
      Typed_ast.lskips ->
      Typed_ast.exp ->
      Typed_ast.lskips ->
      (Typed_ast.const_descr_ref Types.id * Typed_ast.lskips *
       Typed_ast.exp * Ast.l)
      Typed_ast.lskips_seplist ->
      Typed_ast.lskips -> Types.t option -> Typed_ast.exp
    val mk_field :
      Ast.l ->
      Typed_ast.exp ->
      Typed_ast.lskips ->
      Typed_ast.const_descr_ref Types.id -> Types.t option -> Typed_ast.exp
    val mk_case :
      bool ->
      Ast.l ->
      Typed_ast.lskips ->
      Typed_ast.exp ->
      Typed_ast.lskips ->
      (Typed_ast.pat * Typed_ast.lskips * Typed_ast.exp * Ast.l)
      Typed_ast.lskips_seplist ->
      Typed_ast.lskips -> Types.t option -> Typed_ast.exp
    val mk_typed :
      Ast.l ->
      Typed_ast.lskips ->
      Typed_ast.exp ->
      Typed_ast.lskips ->
      Types.src_t -> Typed_ast.lskips -> Types.t option -> Typed_ast.exp
    val mk_let_val :
      Ast.l ->
      Typed_ast.pat ->
      (Typed_ast.lskips * Types.src_t) option ->
      Typed_ast.lskips -> Typed_ast.exp -> Typed_ast.letbind
    val mk_let_fun :
      Ast.l ->
      Typed_ast.name_lskips_annot ->
      Typed_ast.pat list ->
      (Typed_ast.lskips * Types.src_t) option ->
      Typed_ast.lskips -> Typed_ast.exp -> Typed_ast.letbind
    val mk_let :
      Ast.l ->
      Typed_ast.lskips ->
      Typed_ast.letbind ->
      Typed_ast.lskips -> Typed_ast.exp -> Types.t option -> Typed_ast.exp
    val mk_tup :
      Ast.l ->
      Typed_ast.lskips ->
      Typed_ast.exp Typed_ast.lskips_seplist ->
      Typed_ast.lskips -> Types.t option -> Typed_ast.exp
    val mk_list :
      Ast.l ->
      Typed_ast.lskips ->
      Typed_ast.exp Typed_ast.lskips_seplist ->
      Typed_ast.lskips -> Types.t -> Typed_ast.exp
    val mk_vector :
      Ast.l ->
      Typed_ast.lskips ->
      Typed_ast.exp Typed_ast.lskips_seplist ->
      Typed_ast.lskips -> Types.t -> Typed_ast.exp
    val mk_vaccess :
      Ast.l ->
      Typed_ast.exp ->
      Typed_ast.lskips ->
      Types.src_nexp -> Typed_ast.lskips -> Types.t -> Typed_ast.exp
    val mk_vaccessr :
      Ast.l ->
      Typed_ast.exp ->
      Typed_ast.lskips ->
      Types.src_nexp ->
      Typed_ast.lskips ->
      Types.src_nexp -> Typed_ast.lskips -> Types.t -> Typed_ast.exp
    val mk_paren :
      Ast.l ->
      Typed_ast.lskips ->
      Typed_ast.exp -> Typed_ast.lskips -> Types.t option -> Typed_ast.exp
    val mk_begin :
      Ast.l ->
      Typed_ast.lskips ->
      Typed_ast.exp -> Typed_ast.lskips -> Types.t option -> Typed_ast.exp
    val mk_if :
      Ast.l ->
      Typed_ast.lskips ->
      Typed_ast.exp ->
      Typed_ast.lskips ->
      Typed_ast.exp ->
      Typed_ast.lskips -> Typed_ast.exp -> Types.t option -> Typed_ast.exp
    val mk_lit : Ast.l -> Typed_ast.lit -> Types.t option -> Typed_ast.exp
    val mk_set :
      Ast.l ->
      Typed_ast.lskips ->
      Typed_ast.exp Typed_ast.lskips_seplist ->
      Typed_ast.lskips -> Types.t -> Typed_ast.exp
    val mk_setcomp :
      Ast.l ->
      Typed_ast.lskips ->
      Typed_ast.exp ->
      Typed_ast.lskips ->
      Typed_ast.exp ->
      Typed_ast.lskips ->
      Typed_ast.NameSet.t -> Types.t option -> Typed_ast.exp
    val mk_comp_binding :
      Ast.l ->
      bool ->
      Typed_ast.lskips ->
      Typed_ast.exp ->
      Typed_ast.lskips ->
      Typed_ast.lskips ->
      Typed_ast.quant_binding list ->
      Typed_ast.lskips ->
      Typed_ast.exp -> Typed_ast.lskips -> Types.t option -> Typed_ast.exp
    val mk_quant :
      Ast.l ->
      Ast.q ->
      Typed_ast.quant_binding list ->
      Typed_ast.lskips -> Typed_ast.exp -> Types.t option -> Typed_ast.exp
    val mk_do :
      Ast.l ->
      Typed_ast.lskips ->
      Path.t Types.id ->
      Typed_ast.do_line list ->
      Typed_ast.lskips ->
      Typed_ast.exp ->
      Typed_ast.lskips ->
      Types.t * Typed_ast.bind_tyargs_order ->
      Types.t option -> Typed_ast.exp
    val t_to_src_t : Types.t -> Types.src_t
    val pat_subst :
      Types.t Types.TNfmap.t * Name.t Typed_ast.Nfmap.t ->
      Typed_ast.pat -> Typed_ast.pat
  end