Nativecode (coq-core.Nativecode)

type mllambda

type global

val debug_native_compiler : CDebug.t

val keep_debug_files : unit -> bool

val pp_global : Stdlib.Format.formatter -> global -> unit

val mk_open : string -> global

val clear_symbols : unit -> unit

val get_value : Nativevalues.symbols -> int -> Nativevalues.t

val get_sort : Nativevalues.symbols -> int -> Sorts.t

val get_name : Nativevalues.symbols -> int -> Names.Name.t

val get_const : Nativevalues.symbols -> int -> Names.Constant.t

val get_match : Nativevalues.symbols -> int -> Nativevalues.annot_sw

val get_ind : Nativevalues.symbols -> int -> Names.inductive

val get_evar : Nativevalues.symbols -> int -> Evar.t

val get_level : Nativevalues.symbols -> int -> Univ.Level.t

val get_proj : Nativevalues.symbols -> int -> Names.inductive * int

val get_symbols : unit -> Nativevalues.symbols

type code_location_updates

type linkable_code = global list * code_location_updates

val clear_global_tbl : unit -> unit

val empty_updates : code_location_updates

val register_native_file : string -> unit

val is_loaded_native_file : string -> bool

val compile_constant_field : 
  Environ.env ->
  Names.Constant.t ->
  global list ->
  'a Declarations.pconstant_body ->
  global list

val compile_mind_field : 
  Names.ModPath.t ->
  Names.Label.t ->
  global list ->
  Declarations.mutual_inductive_body ->
  global list

val mk_conv_code : 
  Environ.env ->
  Genlambda.evars ->
  string ->
  Constr.constr ->
  Constr.constr ->
  linkable_code

val mk_norm_code : 
  Environ.env ->
  Genlambda.evars ->
  string ->
  Constr.constr ->
  linkable_code

val mk_library_header : Nativevalues.symbols -> global list

val mod_uid_of_dirpath : Names.DirPath.t -> string

val link_info_of_dirpath : Names.DirPath.t -> Environ.link_info

val update_locations : code_location_updates -> unit

val add_header_comment : global list -> string -> global list