package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type reduction_tactic_error =
  1. | InvalidAbstraction of Environ.env * Evd.evar_map * EConstr.constr * Environ.env * Type_errors.type_error
exception ReductionTacticError of reduction_tactic_error
val is_evaluable : Environ.env -> Names.evaluable_global_reference -> bool
val error_not_evaluable : Names.GlobRef.t -> 'a
val evaluable_of_global_reference : Environ.env -> Names.GlobRef.t -> Names.evaluable_global_reference
val global_of_evaluable_reference : Names.evaluable_global_reference -> Names.GlobRef.t
exception Redelimination
val try_red_product : Reductionops.reduction_function
val cbv_betadeltaiota : Reductionops.reduction_function
val reduce_to_quantified_ref : Environ.env -> Evd.evar_map -> Names.GlobRef.t -> EConstr.types -> EConstr.types
val reduce_to_atomic_ref : Environ.env -> Evd.evar_map -> Names.GlobRef.t -> EConstr.types -> EConstr.types