package coq-core

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val compile : fail_on_error:bool -> ?universes:(int * int) -> Environ.env -> Genlambda.evars -> Constr.constr -> (bool array * Vmemitcodes.to_patch * Vmemitcodes.patches) option

Should only be used for monomorphic terms

val compile_constant_body : fail_on_error:bool -> Environ.env -> Declarations.universes -> (Constr.t, 'opaque, 'symb) Declarations.constant_def -> Vmemitcodes.body_code option

Shortcut of the previous function used during module strengthening

val compile_alias : Names.Constant.t -> 'a Vmemitcodes.pbody_code
val dump_bytecode : bool ref

Dump the bytecode after compilation (for debugging purposes)

OCaml

Innovation. Community. Security.