sig
  type defn_ctxt = {
    all_tdefs : Types.type_defs;
    ctxt_c_env : Typed_ast.c_env;
    ctxt_e_env : Typed_ast.mod_descr Types.Pfmap.t;
    all_instances : Types.i_env;
    lemmata_labels : Typed_ast.NameSet.t;
    ctxt_mod_target_rep : Typed_ast.mod_target_rep Target.Targetmap.t;
    ctxt_mod_in_output : bool;
    cur_env : Typed_ast.local_env;
    new_defs : Typed_ast.local_env;
    export_env : Typed_ast.local_env;
    new_tdefs : Path.t list;
    new_instances : Types.instance_ref list;
  }
  val add_d_to_ctxt :
    Typecheck_ctxt.defn_ctxt ->
    Path.t -> Types.tc_def -> Typecheck_ctxt.defn_ctxt
  val add_p_to_ctxt :
    Typecheck_ctxt.defn_ctxt ->
    Name.t * (Path.t * Ast.l) -> Typecheck_ctxt.defn_ctxt
  val add_f_to_ctxt :
    Typecheck_ctxt.defn_ctxt ->
    Name.t * Types.const_descr_ref -> Typecheck_ctxt.defn_ctxt
  val add_v_to_ctxt :
    Typecheck_ctxt.defn_ctxt ->
    Name.t * Types.const_descr_ref -> Typecheck_ctxt.defn_ctxt
  val union_v_ctxt :
    Typecheck_ctxt.defn_ctxt ->
    Typed_ast.const_descr_ref Typed_ast.Nfmap.t -> Typecheck_ctxt.defn_ctxt
  val add_m_to_ctxt :
    Ast.l ->
    Typecheck_ctxt.defn_ctxt ->
    Name.t -> Typed_ast.mod_descr -> Typecheck_ctxt.defn_ctxt
  val add_m_alias_to_ctxt :
    Ast.l ->
    Typecheck_ctxt.defn_ctxt -> Name.t -> Path.t -> Typecheck_ctxt.defn_ctxt
  val add_instance_to_ctxt :
    Typecheck_ctxt.defn_ctxt ->
    Types.instance -> Typecheck_ctxt.defn_ctxt * Types.instance_ref
  val add_lemma_to_ctxt :
    Typecheck_ctxt.defn_ctxt -> Name.t -> Typecheck_ctxt.defn_ctxt
  val defn_ctxt_to_env : Typecheck_ctxt.defn_ctxt -> Typed_ast.env
  val ctxt_c_env_set_target_rep :
    Ast.l ->
    Typecheck_ctxt.defn_ctxt ->
    Typed_ast.const_descr_ref ->
    Target.non_ident_target ->
    Typed_ast.const_target_rep ->
    Typecheck_ctxt.defn_ctxt * Typed_ast.const_target_rep option
  val ctxt_all_tdefs_set_target_rep :
    Ast.l ->
    Typecheck_ctxt.defn_ctxt ->
    Path.t ->
    Target.non_ident_target ->
    Types.type_target_rep ->
    Typecheck_ctxt.defn_ctxt * Types.type_target_rep option
  val ctxt_begin_submodule :
    Typecheck_ctxt.defn_ctxt -> Typecheck_ctxt.defn_ctxt
  val ctxt_end_submodule :
    Ast.l ->
    Typecheck_ctxt.defn_ctxt ->
    Name.t list ->
    Name.t -> Typecheck_ctxt.defn_ctxt -> Typecheck_ctxt.defn_ctxt
end