package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

This file defines the mllambda code generation phase of the native compiler. mllambda represents a fragment of ML, and can easily be printed to OCaml code.

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_ind : Nativevalues.symbols -> int -> Names.inductive
val get_evar : Nativevalues.symbols -> int -> Evar.t
val get_instance : Nativevalues.symbols -> int -> UVars.Instance.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 update_locations : code_location_updates -> unit
val add_header_comment : global list -> string -> global list
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct