package coq

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

type evars = {

}

val empty_evars : evars

val decompose_Llam : 
  Nativeinstr.lambda ->
  Names.name array * Nativeinstr.lambda

val decompose_Llam_Llet : 
  Nativeinstr.lambda ->
  (Names.name * Nativeinstr.lambda option) array * Nativeinstr.lambda

val is_lazy : Nativeinstr.prefix -> Term.constr -> bool

val mk_lazy : Nativeinstr.lambda -> Nativeinstr.lambda

val get_mind_prefix : Pre_env.env -> Names.mutual_inductive -> string

val get_alias : Pre_env.env -> Term.pconstant -> Term.pconstant

val lambda_of_constr : 
  Pre_env.env ->
  evars ->
  Constr.constr ->
  Nativeinstr.lambda

val compile_static_int31 : bool -> Constr.constr array -> Nativeinstr.lambda

val compile_dynamic_int31 : 
  bool ->
  Nativeinstr.prefix ->
  Names.constructor ->
  Nativeinstr.lambda array ->
  Nativeinstr.lambda

val before_match_int31 : 
  Names.inductive ->
  bool ->
  Nativeinstr.prefix ->
  Names.constructor ->
  Nativeinstr.lambda ->
  Nativeinstr.lambda

val compile_prim : 
  Primitives.t ->
  Names.constant ->
  bool ->
  Nativeinstr.prefix ->
  Nativeinstr.lambda array ->
  Nativeinstr.lambda