Module Tacred

type reduction_tactic_error =
| InvalidAbstraction of Environ.env * Evd.evar_map * EConstr.constr * Environ.env * Type_errors.type_error
exception ReductionTacticError of reduction_tactic_error
Reduction functions associated to tactics.
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 red_product : Reductionops.reduction_function

Red (raise user error if nothing reducible)

val try_red_product : Reductionops.reduction_function

Red (raise Redelimination if nothing reducible)

val simpl : Reductionops.reduction_function

Simpl

val whd_simpl : Reductionops.reduction_function

Simpl only at the head

val hnf_constr : Reductionops.reduction_function

Hnf: like whd_simpl but force delta-reduction of constants that do not immediately hide a non reducible fix or cofix

val unfoldn : (Locus.occurrences * Names.evaluable_global_reference) list -> Reductionops.reduction_function

Unfold

val fold_commands : EConstr.constr list -> Reductionops.reduction_function

Fold

val pattern_occs : (Locus.occurrences * EConstr.constr) list -> Reductionops.e_reduction_function

Pattern

val cbv_norm_flags : CClosure.RedFlags.reds -> Reductionops.reduction_function

Call by value strategy (uses Closures)

val cbv_beta : Reductionops.reduction_function
val cbv_betaiota : Reductionops.reduction_function
val cbv_betadeltaiota : Reductionops.reduction_function
val compute : Reductionops.reduction_function

= cbv_betadeltaiota

val reduce_to_atomic_ind : Environ.env -> Evd.evar_map -> EConstr.types -> (Names.inductive * EConstr.EInstance.t) * EConstr.types

reduce_to_atomic_ind env sigma t puts t in the form t'=(I args) with I an inductive definition; returns I and t' or fails with a user error

val reduce_to_quantified_ind : Environ.env -> Evd.evar_map -> EConstr.types -> (Names.inductive * EConstr.EInstance.t) * EConstr.types

reduce_to_quantified_ind env sigma t puts t in the form t'=(x1:A1)..(xn:An)(I args) with I an inductive definition; returns I and t' or fails with a user error

val reduce_to_quantified_ref : Environ.env -> Evd.evar_map -> Names.GlobRef.t -> EConstr.types -> EConstr.types

reduce_to_quantified_ref env sigma ref t try to put t in the form t'=(x1:A1)..(xn:An)(ref args) and fails with user error if not possible

val reduce_to_atomic_ref : Environ.env -> Evd.evar_map -> Names.GlobRef.t -> EConstr.types -> EConstr.types
val find_hnf_rectype : Environ.env -> Evd.evar_map -> EConstr.types -> (Names.inductive * EConstr.EInstance.t) * EConstr.constr list
val contextually : bool -> (Locus.occurrences * Pattern.constr_pattern) -> (Ltac_pretype.patvar_map -> Reductionops.reduction_function) -> Reductionops.reduction_function
val e_contextually : bool -> (Locus.occurrences * Pattern.constr_pattern) -> (Ltac_pretype.patvar_map -> Reductionops.e_reduction_function) -> Reductionops.e_reduction_function
val check_privacy : Environ.env -> Names.inductive Univ.puniverses -> Names.inductive Univ.puniverses

Returns the same inductive if it is allowed for pattern-matching raises an error otherwise. *

val check_not_primitive_record : Environ.env -> Names.inductive Univ.puniverses -> Names.inductive Univ.puniverses

Returns the same inductive if it is not a primitive record raises an error otherwise. *