package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type evars = {
  1. evars_val : Constr.existential -> Constr.constr option;
  2. evars_metas : Constr.metavariable -> Constr.types;
}
val empty_evars : evars
val decompose_Llam : Nativeinstr.lambda -> Names.Name.t array * Nativeinstr.lambda
val decompose_Llam_Llet : Nativeinstr.lambda -> (Names.Name.t * Nativeinstr.lambda option) array * Nativeinstr.lambda
val is_lazy : Environ.env -> Nativeinstr.prefix -> Constr.constr -> bool
val get_mind_prefix : Environ.env -> Names.MutInd.t -> string
val lambda_of_constr : Environ.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