sig
  module NameSet :
    sig
      type elt = Name.t
      type t = Set.Make(Name).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 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 -> 'a) -> t -> 'a -> '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 min_elt : t -> elt
      val max_elt : t -> elt
      val choose : t -> elt
      val split : elt -> t -> t * bool * t
    end
  module Nfmap :
    sig
      type k = Name.t
      module S :
        sig
          type elt = k
          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 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 -> 'a) -> t -> 'a -> '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 min_elt : t -> elt
          val max_elt : t -> elt
          val choose : t -> elt
          val split : elt -> t -> t * bool * t
        end
      type 'a t
      val empty : 'a t
      val is_empty : 'a t -> bool
      val from_list : (k * 'a) list -> 'a t
      val from_list2 : k list -> 'a list -> 'a t
      val insert : 'a t -> k * 'a -> 'a t
      val union : 'a t -> 'a t -> 'a t
      val big_union : 'a t list -> 'a t
      val merge :
        (k -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
      val apply : 'a t -> k -> 'a option
      val in_dom : k -> 'a t -> bool
      val map : (k -> 'a -> 'b) -> 'a t -> 'b t
      val domains_overlap : 'a t -> 'b t -> k option
      val domains_disjoint : 'a t list -> bool
      val iter : (k -> 'a -> unit) -> 'a t -> unit
      val fold : ('a -> k -> 'b -> 'a) -> 'a -> 'b t -> 'a
      val filter : (k -> 'a -> bool) -> 'a t -> 'a t
      val remove : 'a t -> k -> 'a t
      val pp_map :
        (Format.formatter -> k -> unit) ->
        (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
      val domain : 'a t -> S.t
    end
  val nfmap_domain : 'a Typed_ast.Nfmap.t -> Typed_ast.NameSet.t
  type name_l = Name.lskips_t * Ast.l
  type lskips = Ast.lex_skips
  type 'a lskips_seplist = ('a, Typed_ast.lskips) Seplist.t
  val no_lskips : Typed_ast.lskips
  val space : Typed_ast.lskips
  val lskips_only_comments : Typed_ast.lskips list -> Typed_ast.lskips
  val lskips_only_comments_first : Typed_ast.lskips list -> Typed_ast.lskips
  type env_tag =
      K_let
    | K_field
    | K_constr
    | K_relation
    | K_method
    | K_instance
  type p_env = (Path.t * Ast.l) Typed_ast.Nfmap.t
  type lit = (Typed_ast.lit_aux, unit) Types.annot
  and lit_aux =
      L_true of Typed_ast.lskips
    | L_false of Typed_ast.lskips
    | L_zero of Typed_ast.lskips
    | L_one of Typed_ast.lskips
    | L_numeral of Typed_ast.lskips * int
    | L_num of Typed_ast.lskips * int
    | L_char of Typed_ast.lskips * char
    | L_string of Typed_ast.lskips * string
    | L_unit of Typed_ast.lskips * Typed_ast.lskips
    | L_vector of Typed_ast.lskips * string * string
    | L_undefined of Typed_ast.lskips * string
  type const_descr_ref = Types.const_descr_ref
  type name_kind =
      Nk_typeconstr of Path.t
    | Nk_const of Typed_ast.const_descr_ref
    | Nk_constr of Typed_ast.const_descr_ref
    | Nk_field of Typed_ast.const_descr_ref
    | Nk_module of Path.t
    | Nk_class of Path.t
  type pat = (Typed_ast.pat_aux, Typed_ast.pat_annot) Types.annot
  and pat_annot = { pvars : Types.t Typed_ast.Nfmap.t; }
  and pat_aux =
      P_wild of Typed_ast.lskips
    | P_as of Typed_ast.lskips * Typed_ast.pat * Typed_ast.lskips *
        Typed_ast.name_l * Typed_ast.lskips
    | P_typ of Typed_ast.lskips * Typed_ast.pat * Typed_ast.lskips *
        Types.src_t * Typed_ast.lskips
    | P_var of Name.lskips_t
    | P_const of Typed_ast.const_descr_ref Types.id * Typed_ast.pat list
    | P_backend of Typed_ast.lskips * Ident.t * Types.t * Typed_ast.pat list
    | P_record of Typed_ast.lskips *
        (Typed_ast.const_descr_ref Types.id * Typed_ast.lskips *
         Typed_ast.pat)
        Typed_ast.lskips_seplist * Typed_ast.lskips
    | P_vector of Typed_ast.lskips * Typed_ast.pat Typed_ast.lskips_seplist *
        Typed_ast.lskips
    | P_vectorC of Typed_ast.lskips * Typed_ast.pat list * Typed_ast.lskips
    | P_tup of Typed_ast.lskips * Typed_ast.pat Typed_ast.lskips_seplist *
        Typed_ast.lskips
    | P_list of Typed_ast.lskips * Typed_ast.pat Typed_ast.lskips_seplist *
        Typed_ast.lskips
    | P_paren of Typed_ast.lskips * Typed_ast.pat * Typed_ast.lskips
    | P_cons of Typed_ast.pat * Typed_ast.lskips * Typed_ast.pat
    | P_num_add of Typed_ast.name_l * Typed_ast.lskips * Typed_ast.lskips *
        int
    | P_lit of Typed_ast.lit
    | P_var_annot of Name.lskips_t * Types.src_t
  and cr_special_fun =
      CR_special_uncurry of int
    | CR_special_rep of string list * Typed_ast.exp list
  and const_target_rep =
      CR_inline of Ast.l * bool * Typed_ast.name_lskips_annot list *
        Typed_ast.exp
    | CR_infix of Ast.l * bool * Ast.fixity_decl * Ident.t
    | CR_undefined of Ast.l * bool
    | CR_simple of Ast.l * bool * Typed_ast.name_lskips_annot list *
        Typed_ast.exp
    | CR_special of Ast.l * bool * Typed_ast.cr_special_fun *
        Typed_ast.name_lskips_annot list
  and rel_io = Rel_mode_in | Rel_mode_out
  and rel_mode = Typed_ast.rel_io list
  and rel_output_type = Out_list | Out_pure | Out_option | Out_unique
  and rel_info = {
    ri_witness :
      (Path.t * Typed_ast.const_descr_ref Typed_ast.Nfmap.t) option;
    ri_check : Typed_ast.const_descr_ref option;
    ri_fns :
      ((Typed_ast.rel_mode * bool * Typed_ast.rel_output_type) *
       Typed_ast.const_descr_ref)
      list;
  }
  and const_descr = {
    const_binding : Path.t;
    const_tparams : Types.tnvar list;
    const_class : (Path.t * Types.tnvar) list;
    const_no_class : Typed_ast.const_descr_ref Target.Targetmap.t;
    const_ranges : Types.range list;
    const_type : Types.t;
    relation_info : Typed_ast.rel_info option;
    env_tag : Typed_ast.env_tag;
    const_targets : Target.Targetset.t;
    spec_l : Ast.l;
    target_rename : (Ast.l * Name.t) Target.Targetmap.t;
    target_ascii_rep : (Ast.l * Name.t) Target.Targetmap.t;
    target_rep : Typed_ast.const_target_rep Target.Targetmap.t;
    compile_message : string Target.Targetmap.t;
    termination_setting : Ast.termination_setting Target.Targetmap.t;
  }
  and v_env = Typed_ast.const_descr_ref Typed_ast.Nfmap.t
  and f_env = Typed_ast.const_descr_ref Typed_ast.Nfmap.t
  and m_env = Path.t Typed_ast.Nfmap.t
  and e_env = Typed_ast.mod_descr Types.Pfmap.t
  and c_env
  and local_env = {
    m_env : Typed_ast.m_env;
    p_env : Typed_ast.p_env;
    f_env : Typed_ast.f_env;
    v_env : Typed_ast.v_env;
  }
  and env = {
    local_env : Typed_ast.local_env;
    c_env : Typed_ast.c_env;
    t_env : Types.type_defs;
    i_env : Types.i_env;
    e_env : Typed_ast.e_env;
  }
  and mod_target_rep = MR_rename of Ast.l * Name.t
  and mod_descr = {
    mod_binding : Path.t;
    mod_env : Typed_ast.local_env;
    mod_target_rep : Typed_ast.mod_target_rep Target.Targetmap.t;
    mod_filename : string option;
    mod_in_output : bool;
  }
  and exp
  and exp_subst = Sub of Typed_ast.exp | Sub_rename of Name.t
  and exp_aux = private
      Var of Name.lskips_t
    | Backend of Typed_ast.lskips * Ident.t
    | Nvar_e of Typed_ast.lskips * Nvar.t
    | Constant of Typed_ast.const_descr_ref Types.id
    | Fun of Typed_ast.lskips * Typed_ast.pat list * Typed_ast.lskips *
        Typed_ast.exp
    | Function of Typed_ast.lskips *
        (Typed_ast.pat * Typed_ast.lskips * Typed_ast.exp * Ast.l)
        Typed_ast.lskips_seplist * Typed_ast.lskips
    | App of Typed_ast.exp * Typed_ast.exp
    | Infix of Typed_ast.exp * Typed_ast.exp * Typed_ast.exp
    | Record of Typed_ast.lskips * Typed_ast.fexp Typed_ast.lskips_seplist *
        Typed_ast.lskips
    | Recup of Typed_ast.lskips * Typed_ast.exp * Typed_ast.lskips *
        Typed_ast.fexp Typed_ast.lskips_seplist * Typed_ast.lskips
    | Field of Typed_ast.exp * Typed_ast.lskips *
        Typed_ast.const_descr_ref Types.id
    | Vector of Typed_ast.lskips * Typed_ast.exp Typed_ast.lskips_seplist *
        Typed_ast.lskips
    | VectorSub of Typed_ast.exp * Typed_ast.lskips * Types.src_nexp *
        Typed_ast.lskips * Types.src_nexp * Typed_ast.lskips
    | VectorAcc of Typed_ast.exp * Typed_ast.lskips * Types.src_nexp *
        Typed_ast.lskips
    | Case of bool * 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
    | Typed of Typed_ast.lskips * Typed_ast.exp * Typed_ast.lskips *
        Types.src_t * Typed_ast.lskips
    | Let of Typed_ast.lskips * Typed_ast.letbind * Typed_ast.lskips *
        Typed_ast.exp
    | Tup of Typed_ast.lskips * Typed_ast.exp Typed_ast.lskips_seplist *
        Typed_ast.lskips
    | List of Typed_ast.lskips * Typed_ast.exp Typed_ast.lskips_seplist *
        Typed_ast.lskips
    | Paren of Typed_ast.lskips * Typed_ast.exp * Typed_ast.lskips
    | Begin of Typed_ast.lskips * Typed_ast.exp * Typed_ast.lskips
    | If of Typed_ast.lskips * Typed_ast.exp * Typed_ast.lskips *
        Typed_ast.exp * Typed_ast.lskips * Typed_ast.exp
    | Lit of Typed_ast.lit
    | Set of Typed_ast.lskips * Typed_ast.exp Typed_ast.lskips_seplist *
        Typed_ast.lskips
    | Setcomp of Typed_ast.lskips * Typed_ast.exp * Typed_ast.lskips *
        Typed_ast.exp * Typed_ast.lskips * Typed_ast.NameSet.t
    | Comp_binding of 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
    | Quant of Ast.q * Typed_ast.quant_binding list * Typed_ast.lskips *
        Typed_ast.exp
    | Do of 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)
  and do_line =
      Do_line of
        (Typed_ast.pat * Typed_ast.lskips * Typed_ast.exp * Typed_ast.lskips)
  and bind_tyargs_order = BTO_input_output | BTO_output_input
  and fexp =
      Typed_ast.const_descr_ref Types.id * Typed_ast.lskips * Typed_ast.exp *
      Ast.l
  and name_lskips_annot = (Name.lskips_t, unit) Types.annot
  and quant_binding =
      Qb_var of Typed_ast.name_lskips_annot
    | Qb_restr of bool * Typed_ast.lskips * Typed_ast.pat *
        Typed_ast.lskips * Typed_ast.exp * Typed_ast.lskips
  and funcl_aux =
      Typed_ast.name_lskips_annot * Typed_ast.const_descr_ref *
      Typed_ast.pat list * (Typed_ast.lskips * Types.src_t) option *
      Typed_ast.lskips * Typed_ast.exp
  and letbind = Typed_ast.letbind_aux * Ast.l
  and letbind_aux =
      Let_val of Typed_ast.pat * (Typed_ast.lskips * Types.src_t) option *
        Typed_ast.lskips * Typed_ast.exp
    | Let_fun of Typed_ast.name_lskips_annot * Typed_ast.pat list *
        (Typed_ast.lskips * Types.src_t) option * Typed_ast.lskips *
        Typed_ast.exp
  type tyvar = Typed_ast.lskips * Ulib.Text.t * Ast.l
  type nvar = Typed_ast.lskips * Ulib.Text.t * Ast.l
  type tnvar = Tn_A of Typed_ast.tyvar | Tn_N of Typed_ast.nvar
  type texp =
      Te_opaque
    | Te_abbrev of Typed_ast.lskips * Types.src_t
    | Te_record of Typed_ast.lskips * Typed_ast.lskips *
        (Typed_ast.name_l * Typed_ast.const_descr_ref * Typed_ast.lskips *
         Types.src_t)
        Typed_ast.lskips_seplist * Typed_ast.lskips
    | Te_variant of Typed_ast.lskips *
        (Typed_ast.name_l * Typed_ast.const_descr_ref * Typed_ast.lskips *
         Types.src_t Typed_ast.lskips_seplist)
        Typed_ast.lskips_seplist
  type range =
      GtEq of Ast.l * Types.src_nexp * Typed_ast.lskips * Types.src_nexp
    | Eq of Ast.l * Types.src_nexp * Typed_ast.lskips * Types.src_nexp
  type constraints =
      Cs_list of (Ident.t * Typed_ast.tnvar) Typed_ast.lskips_seplist *
        Typed_ast.lskips option * Typed_ast.range Typed_ast.lskips_seplist *
        Typed_ast.lskips
  type constraint_prefix =
      Cp_forall of Typed_ast.lskips * Typed_ast.tnvar list *
        Typed_ast.lskips * Typed_ast.constraints option
  type typschm = Typed_ast.constraint_prefix option * Types.src_t
  type instschm =
      Typed_ast.constraint_prefix option * Typed_ast.lskips * Ident.t *
      Path.t * Types.src_t * Typed_ast.lskips
  val cr_special_fun_uses_name : Typed_ast.cr_special_fun -> bool
  type targets_opt =
      (bool * Typed_ast.lskips * Ast.target Typed_ast.lskips_seplist *
       Typed_ast.lskips)
      option
  val in_targets_opt : Target.target -> Typed_ast.targets_opt -> bool
  val in_target_set : Target.target -> Target.Targetset.t -> bool
  val targets_opt_to_list :
    Typed_ast.targets_opt -> Target.non_ident_target list
  type val_spec =
      Typed_ast.lskips * Typed_ast.name_l * Typed_ast.const_descr_ref *
      Ast.ascii_opt * Typed_ast.lskips * Typed_ast.typschm
  type class_val_spec =
      Typed_ast.lskips * Typed_ast.targets_opt * Typed_ast.name_l *
      Typed_ast.const_descr_ref * Ast.ascii_opt * Typed_ast.lskips *
      Types.src_t
  type fun_def_rec_flag = FR_non_rec | FR_rec of Typed_ast.lskips
  type val_def =
      Let_def of Typed_ast.lskips * Typed_ast.targets_opt *
        (Typed_ast.pat * (Name.t * Typed_ast.const_descr_ref) list *
         (Typed_ast.lskips * Types.src_t) option * Typed_ast.lskips *
         Typed_ast.exp)
    | Fun_def of Typed_ast.lskips * Typed_ast.fun_def_rec_flag *
        Typed_ast.targets_opt * Typed_ast.funcl_aux Typed_ast.lskips_seplist
    | Let_inline of Typed_ast.lskips * Typed_ast.lskips *
        Typed_ast.targets_opt * Typed_ast.name_lskips_annot *
        Typed_ast.const_descr_ref * Typed_ast.name_lskips_annot list *
        Typed_ast.lskips * Typed_ast.exp
  type name_sect =
      Name_restrict of
        (Typed_ast.lskips * Typed_ast.name_l * Typed_ast.lskips *
         Typed_ast.lskips * string * Typed_ast.lskips)
  type indreln_rule_quant_name =
      QName of Typed_ast.name_lskips_annot
    | Name_typ of Typed_ast.lskips * Typed_ast.name_lskips_annot *
        Typed_ast.lskips * Types.src_t * Typed_ast.lskips
  type indreln_rule_aux =
      Rule of Name.lskips_t * Typed_ast.lskips * Typed_ast.lskips *
        Typed_ast.indreln_rule_quant_name list * Typed_ast.lskips *
        Typed_ast.exp option * Typed_ast.lskips *
        Typed_ast.name_lskips_annot * Typed_ast.const_descr_ref *
        Typed_ast.exp list
  type indreln_rule = Typed_ast.indreln_rule_aux * Ast.l
  type indreln_witness =
      Indreln_witness of Typed_ast.lskips * Typed_ast.lskips *
        Name.lskips_t * Typed_ast.lskips
  type indreln_indfn =
      Indreln_fn of Name.lskips_t * Typed_ast.lskips * Types.src_t *
        Typed_ast.lskips option
  type indreln_name =
      RName of Typed_ast.lskips * Name.lskips_t * Typed_ast.const_descr_ref *
        Typed_ast.lskips * Typed_ast.typschm *
        Typed_ast.indreln_witness option *
        (Typed_ast.lskips * Name.lskips_t * Typed_ast.lskips) option *
        Typed_ast.indreln_indfn list option * Typed_ast.lskips
  type target_rep_rhs =
      Target_rep_rhs_infix of Typed_ast.lskips * Ast.fixity_decl *
        Typed_ast.lskips * Ident.t
    | Target_rep_rhs_term_replacement of Typed_ast.exp
    | Target_rep_rhs_type_replacement of Types.src_t
    | Target_rep_rhs_special of Typed_ast.lskips * Typed_ast.lskips *
        string * Typed_ast.exp list
    | Target_rep_rhs_undefined
  type declare_def =
      Decl_compile_message of Typed_ast.lskips * Typed_ast.targets_opt *
        Typed_ast.lskips * Typed_ast.const_descr_ref Types.id *
        Typed_ast.lskips * Typed_ast.lskips * string
    | Decl_target_rep_term of Typed_ast.lskips * Ast.target *
        Typed_ast.lskips * Ast.component *
        Typed_ast.const_descr_ref Types.id *
        Typed_ast.name_lskips_annot list * Typed_ast.lskips *
        Typed_ast.target_rep_rhs
    | Decl_target_rep_type of Typed_ast.lskips * Ast.target *
        Typed_ast.lskips * Typed_ast.lskips * Path.t Types.id *
        Typed_ast.tnvar list * Typed_ast.lskips * Types.src_t
    | Decl_ascii_rep of Typed_ast.lskips * Typed_ast.targets_opt *
        Typed_ast.lskips * Ast.component * Typed_ast.name_kind Types.id *
        Typed_ast.lskips * Typed_ast.lskips * Name.t
    | Decl_rename of Typed_ast.lskips * Typed_ast.targets_opt *
        Typed_ast.lskips * Ast.component * Typed_ast.name_kind Types.id *
        Typed_ast.lskips * Name.lskips_t
    | Decl_rename_current_module of Typed_ast.lskips *
        Typed_ast.targets_opt * Typed_ast.lskips * Typed_ast.lskips *
        Typed_ast.lskips * Name.lskips_t
    | Decl_termination_argument of Typed_ast.lskips * Typed_ast.targets_opt *
        Typed_ast.lskips * Typed_ast.const_descr_ref Types.id *
        Typed_ast.lskips * Ast.termination_setting
    | Decl_pattern_match_decl of Typed_ast.lskips * Typed_ast.targets_opt *
        Typed_ast.lskips * Ast.exhaustivity_setting * Path.t Types.id *
        Typed_ast.tnvar list * Typed_ast.lskips * Typed_ast.lskips *
        Typed_ast.const_descr_ref Types.id Typed_ast.lskips_seplist *
        Typed_ast.lskips * Typed_ast.const_descr_ref Types.id option
  type def_aux =
      Type_def of Typed_ast.lskips *
        (Typed_ast.name_l * Typed_ast.tnvar list * Path.t * Typed_ast.texp *
         Typed_ast.name_sect option)
        Typed_ast.lskips_seplist
    | Val_def of Typed_ast.val_def
    | Lemma of Typed_ast.lskips * Ast.lemma_typ * Typed_ast.targets_opt *
        Typed_ast.name_l * Typed_ast.lskips * Typed_ast.exp
    | Module of Typed_ast.lskips * Typed_ast.name_l * Path.t *
        Typed_ast.lskips * Typed_ast.lskips * Typed_ast.def list *
        Typed_ast.lskips
    | Rename of Typed_ast.lskips * Typed_ast.name_l * Path.t *
        Typed_ast.lskips * Path.t Types.id
    | OpenImport of Ast.open_import * Path.t Types.id list
    | OpenImportTarget of Ast.open_import * Typed_ast.targets_opt *
        (Typed_ast.lskips * string) list
    | Indreln of Typed_ast.lskips * Typed_ast.targets_opt *
        Typed_ast.indreln_name Typed_ast.lskips_seplist *
        Typed_ast.indreln_rule Typed_ast.lskips_seplist
    | Val_spec of Typed_ast.val_spec
    | Class of Ast.class_decl * Typed_ast.lskips * Typed_ast.name_l *
        Typed_ast.tnvar * Path.t * Typed_ast.lskips *
        Typed_ast.class_val_spec list * Typed_ast.lskips
    | Instance of Ast.instance_decl * Types.instance_ref *
        Typed_ast.instschm * Typed_ast.val_def list * Typed_ast.lskips
    | Comment of Typed_ast.def
    | Declaration of Typed_ast.declare_def
  and def =
      (Typed_ast.def_aux * Typed_ast.lskips option) * Ast.l *
      Typed_ast.local_env
  val tnvar_to_types_tnvar : Typed_ast.tnvar -> Types.tnvar * Ast.l
  val empty_local_env : Typed_ast.local_env
  val empty_env : Typed_ast.env
  val e_env_lookup :
    Ast.l -> Typed_ast.e_env -> Path.t -> Typed_ast.mod_descr
  val c_env_lookup :
    Ast.l ->
    Typed_ast.c_env -> Typed_ast.const_descr_ref -> Typed_ast.const_descr
  val c_env_store_raw :
    Typed_ast.c_env ->
    Typed_ast.const_descr -> Typed_ast.c_env * Typed_ast.const_descr_ref
  val c_env_update :
    Typed_ast.c_env ->
    Typed_ast.const_descr_ref -> Typed_ast.const_descr -> Typed_ast.c_env
  val env_c_env_update :
    Typed_ast.env ->
    Typed_ast.const_descr_ref -> Typed_ast.const_descr -> Typed_ast.env
  val c_env_all_consts : Typed_ast.c_env -> Typed_ast.const_descr_ref list
  val exp_to_locn : Typed_ast.exp -> Ast.l
  val exp_to_typ : Typed_ast.exp -> Types.t
  val append_lskips : Typed_ast.lskips -> Typed_ast.exp -> Typed_ast.exp
  val pat_append_lskips : Typed_ast.lskips -> Typed_ast.pat -> Typed_ast.pat
  val alter_init_lskips :
    (Typed_ast.lskips -> Typed_ast.lskips * Typed_ast.lskips) ->
    Typed_ast.exp -> Typed_ast.exp * Typed_ast.lskips
  val pat_alter_init_lskips :
    (Typed_ast.lskips -> Typed_ast.lskips * Typed_ast.lskips) ->
    Typed_ast.pat -> Typed_ast.pat * Typed_ast.lskips
  val def_aux_alter_init_lskips :
    (Typed_ast.lskips -> Typed_ast.lskips * Typed_ast.lskips) ->
    Typed_ast.def_aux -> Typed_ast.def_aux * Typed_ast.lskips
  val def_alter_init_lskips :
    (Typed_ast.lskips -> Typed_ast.lskips * Typed_ast.lskips) ->
    Typed_ast.def -> Typed_ast.def * Typed_ast.lskips
  val oi_alter_init_lskips :
    (Typed_ast.lskips -> Typed_ast.lskips * Typed_ast.lskips) ->
    Ast.open_import -> Ast.open_import * Typed_ast.lskips
  val pp_const_descr : Format.formatter -> Typed_ast.const_descr -> unit
  val pp_env : Format.formatter -> Typed_ast.env -> unit
  val pp_local_env : Format.formatter -> Typed_ast.local_env -> unit
  val pp_c_env : Format.formatter -> Typed_ast.c_env -> unit
  val pp_instances :
    Format.formatter -> Types.instance list Types.Pfmap.t -> unit
  type imported_modules =
      IM_paths of Path.t list
    | IM_targets of Typed_ast.targets_opt * string list
  type checked_module = {
    filename : string;
    module_path : Path.t;
    imported_modules : Typed_ast.imported_modules list;
    imported_modules_rec : Typed_ast.imported_modules list;
    untyped_ast : Ast.defs * Ast.lex_skips;
    typed_ast : Typed_ast.def list * Ast.lex_skips;
    generate_output : bool;
  }
  type var_avoid_f =
      bool * (Name.t -> bool) * (Ulib.Text.t -> (Name.t -> bool) -> Name.t)
  module type Exp_context =
    sig
      val env_opt : Typed_ast.env option
      val avoid : Typed_ast.var_avoid_f option
    end
  module Exps_in_context :
    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
  val local_env_union :
    Typed_ast.local_env -> Typed_ast.local_env -> Typed_ast.local_env
  val funcl_aux_seplist_group :
    Typed_ast.funcl_aux Typed_ast.lskips_seplist ->
    bool * Typed_ast.lskips option *
    (Name.t * Typed_ast.funcl_aux Typed_ast.lskips_seplist) list
  val class_path_to_dict_name : Path.t -> Types.tnvar -> Name.t
  val ident_get_lskip : 'a Types.id -> Ast.lex_skips
  val ident_replace_lskip :
    Types.ident_option -> Ast.lex_skips -> Types.ident_option
  val oi_get_lskip : Ast.open_import -> Ast.lex_skips
end