package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
exception Elimconst
module ReductionBehaviour : sig ... end
type effect_name = string
val declare_reduction_effect : effect_name -> (Environ.env -> Evd.evar_map -> Constr.constr -> unit) -> unit
val set_reduction_effect : Names.Constant.t -> effect_name -> unit
val reduction_effect_hook : Environ.env -> Evd.evar_map -> Names.Constant.t -> Constr.constr Lazy.t -> unit
module Cst_stack : sig ... end
module Stack : sig ... end
type contextual_reduction_function = Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr
type reduction_function = contextual_reduction_function
type local_reduction_function = Evd.evar_map -> EConstr.constr -> EConstr.constr
type e_reduction_function = Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.constr
type contextual_stack_reduction_function = Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr * EConstr.constr list
type stack_reduction_function = contextual_stack_reduction_function
type local_stack_reduction_function = Evd.evar_map -> EConstr.constr -> EConstr.constr * EConstr.constr list
type contextual_state_reduction_function = Environ.env -> Evd.evar_map -> state -> state
type state_reduction_function = contextual_state_reduction_function
type local_state_reduction_function = Evd.evar_map -> state -> state
val pr_state : Environ.env -> Evd.evar_map -> state -> Pp.t
val stacklam : (state -> 'a) -> EConstr.constr list -> Evd.evar_map -> EConstr.constr -> EConstr.constr Stack.t -> 'a
val whd_state_gen : ?csts:Cst_stack.t -> refold:bool -> tactic_mode:bool -> CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> state -> state * Cst_stack.t
val nf_beta : reduction_function
val nf_betaiota : reduction_function
val nf_betaiotazeta : reduction_function
val nf_all : reduction_function
val whd_nored : local_reduction_function
val whd_betaiota : local_reduction_function
val whd_betaiotazeta : local_reduction_function
val whd_betalet : local_reduction_function
val whd_nored_stack : local_stack_reduction_function
val whd_beta_stack : local_stack_reduction_function
val whd_betaiota_stack : local_stack_reduction_function
val whd_betaiotazeta_stack : local_stack_reduction_function
val whd_allnolet_stack : contextual_stack_reduction_function
val whd_betalet_stack : local_stack_reduction_function
val whd_nored_state : local_state_reduction_function
val whd_beta_state : local_state_reduction_function
val whd_betaiota_state : local_state_reduction_function
val whd_betaiotazeta_state : local_state_reduction_function
val whd_allnolet_state : contextual_state_reduction_function
val whd_betalet_state : local_state_reduction_function
val whd_delta_stack : stack_reduction_function
val whd_delta_state : state_reduction_function
val whd_delta : reduction_function
val whd_betadeltazeta_stack : stack_reduction_function
val whd_betadeltazeta_state : state_reduction_function
val whd_betadeltazeta : reduction_function
val whd_zeta_stack : local_stack_reduction_function
val whd_zeta_state : local_state_reduction_function
val shrink_eta : EConstr.constr -> EConstr.constr
val safe_evar_value : Evd.evar_map -> Constr.existential -> Constr.constr option
val beta_applist : Evd.evar_map -> (EConstr.constr * EConstr.constr list) -> EConstr.constr
val hnf_prod_appvect : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr array -> EConstr.constr
val hnf_prod_applist : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr list -> EConstr.constr
val hnf_lam_appvect : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr array -> EConstr.constr
type !'a miota_args = {
  1. mP : EConstr.constr;
  2. mconstr : EConstr.constr;
  3. mci : Constr.case_info;
  4. mcargs : 'a list;
  5. mlf : 'a array;
}
val reducible_mind_case : Evd.evar_map -> EConstr.constr -> bool
val is_arity : Environ.env -> Evd.evar_map -> EConstr.constr -> bool
val is_sort : Environ.env -> Evd.evar_map -> EConstr.types -> bool
val contract_fix : ?env:Environ.env -> Evd.evar_map -> ?reference:Names.Constant.t -> EConstr.fixpoint -> EConstr.constr
val fix_recarg : ('a, 'a) Constr.pfixpoint -> 'b Stack.t -> (int * 'b) option
val is_transparent : Environ.env -> Names.Constant.t Names.tableKey -> bool
type conversion_test = Univ.Constraint.t -> Univ.Constraint.t
val pb_is_equal : Evd.conv_pb -> bool
val pb_equal : Evd.conv_pb -> Evd.conv_pb
val infer_conv : ?catch_incon:bool -> ?pb:Evd.conv_pb -> ?ts:Names.transparent_state -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> Evd.evar_map option
val set_vm_infer_conv : (?pb:Evd.conv_pb -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> Evd.evar_map option) -> unit
val vm_infer_conv : ?pb:Evd.conv_pb -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> Evd.evar_map option
val head_unfold_under_prod : Names.transparent_state -> reduction_function
val betazetaevar_applist : Evd.evar_map -> int -> EConstr.constr -> EConstr.constr list -> EConstr.constr
val whd_betaiota_deltazeta_for_iota_state : Names.transparent_state -> Environ.env -> Evd.evar_map -> Cst_stack.t -> state -> state * Cst_stack.t
val meta_reducible_instance : Evd.evar_map -> EConstr.constr Evd.freelisted -> EConstr.constr