package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val compile : fail_on_error:bool -> ?universes:int -> Environ.env -> Constr.constr -> (Cbytecodes.bytecodes * Cbytecodes.bytecodes * Cbytecodes.fv) option
val compile_constant_body : fail_on_error:bool -> Environ.env -> Declarations.constant_universes -> Declarations.constant_def -> Cemitcodes.body_code option
val compile_alias : Names.Constant.t -> Cemitcodes.body_code
val dump_bytecode : bool ref