package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type mllambda
type global
val pp_global : Format.formatter -> global -> unit
val mk_open : string -> global
type symbol
type symbols
val empty_symbols : symbols
val clear_symbols : unit -> unit
val get_value : symbols -> int -> Nativevalues.t
val get_sort : symbols -> int -> Sorts.t
val get_name : symbols -> int -> Names.Name.t
val get_const : symbols -> int -> Names.Constant.t
val get_match : symbols -> int -> Nativevalues.annot_sw
val get_ind : symbols -> int -> Names.inductive
val get_meta : symbols -> int -> Constr.metavariable
val get_evar : symbols -> int -> Evar.t
val get_level : symbols -> int -> Univ.Level.t
val get_symbols : unit -> symbols
type code_location_update
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 compile_constant_field : Pre_env.env -> string -> Names.Constant.t -> global list -> Declarations.constant_body -> global list
val compile_mind_field : string -> Names.ModPath.t -> Names.Label.t -> global list -> Declarations.mutual_inductive_body -> global list
val mk_norm_code : Pre_env.env -> Nativelambda.evars -> string -> Constr.constr -> linkable_code
val mk_library_header : Names.DirPath.t -> 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