package coq

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

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 -> Term.sorts

val get_name : symbols -> int -> Names.name

val get_const : symbols -> int -> Names.constant

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

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

val get_meta : symbols -> int -> Term.metavariable

val get_evar : symbols -> int -> Term.existential

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 ->
  global list ->
  Declarations.constant_body ->
  global list

val compile_mind_field : 
  string ->
  Names.module_path ->
  Names.label ->
  global list ->
  Declarations.mutual_inductive_body ->
  global list

val mk_conv_code : 
  Pre_env.env ->
  Nativelambda.evars ->
  string ->
  Term.constr ->
  Term.constr ->
  linkable_code

val mk_norm_code : 
  Pre_env.env ->
  Nativelambda.evars ->
  string ->
  Term.constr ->
  linkable_code

val mk_library_header : Names.dir_path -> global list

val mod_uid_of_dirpath : Names.dir_path -> string

val link_info_of_dirpath : Names.dir_path -> Pre_env.link_info

val update_locations : code_location_updates -> unit

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