Tacredval eq_egr : evaluable_global_reference -> evaluable_global_reference -> boolval subst_evaluable_reference : Mod_subst.substitution -> evaluable_global_reference -> evaluable_global_referenceHere the semantics is completely unclear. What does "Hint Unfold t" means when "t" is a parameter? Does the user mean "Unfold X.t" or does she mean "Unfold y" where X.t is later on instantiated with y? I choose the first interpretation (i.e. an evaluable reference is never expanded).
type reduction_tactic_error = | InvalidAbstraction of Environ.env * Evd.evar_map * EConstr.constr * Environ.env * Type_errors.type_error |
exception ReductionTacticError of reduction_tactic_errorEvaluable global reference
val is_evaluable : Environ.env -> evaluable_global_reference -> boolval error_not_evaluable : Names.GlobRef.t -> 'aval evaluable_of_global_reference : Environ.env -> Names.GlobRef.t -> evaluable_global_referenceval global_of_evaluable_reference : evaluable_global_reference -> Names.GlobRef.tval red_product : Reductionops.reduction_functionRed (raise user error if nothing reducible)
val try_red_product : Reductionops.reduction_functionRed (raise Redelimination if nothing reducible)
val simpl : Reductionops.reduction_functionSimpl
val whd_simpl : Reductionops.reduction_functionSimpl only at the head
val hnf_constr : Reductionops.reduction_functionHnf: like whd_simpl but force delta-reduction of constants that do not immediately hide a non reducible fix or cofix
val hnf_constr0 : Reductionops.reduction_functionVariant of the above that does not perform nf-βι
val unfoldn : (Locus.occurrences * evaluable_global_reference) list -> Reductionops.reduction_functionUnfold
val fold_commands : EConstr.constr list -> Reductionops.reduction_functionFold
val pattern_occs : (Locus.occurrences * EConstr.constr) list -> Reductionops.e_reduction_functionPattern
Rem: Lazy strategies are defined in Reduction
val cbv_norm_flags : CClosure.RedFlags.reds -> Reductionops.reduction_functionCall by value strategy (uses Closures)
val cbv_beta : Reductionops.reduction_functionval cbv_betaiota : Reductionops.reduction_functionval cbv_betadeltaiota : Reductionops.reduction_functionval compute : Reductionops.reduction_function= cbv_betadeltaiota
val reduce_to_atomic_ind : Environ.env -> Evd.evar_map -> EConstr.types -> (Names.inductive * EConstr.EInstance.t) * EConstr.typesreduce_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.typesreduce_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 eval_to_quantified_ind : Environ.env -> Evd.evar_map -> EConstr.types -> Names.inductive * EConstr.EInstance.tSame as reduce_to_quantified_ind but more efficient because it does not return the normalized type.
val reduce_to_quantified_ref : ?allow_failure:bool -> Environ.env -> Evd.evar_map -> Names.GlobRef.t -> EConstr.types -> EConstr.typesreduce_to_quantified_ref env sigma ref t try to put t in the form t'=(x1:A1)..(xn:An)(ref args). When this is not possible, if allow_failure is specified, t is unfolded until the point where this impossibility is plainly visible. Otherwise, it fails with user error.
val reduce_to_atomic_ref : ?allow_failure:bool -> Environ.env -> Evd.evar_map -> Names.GlobRef.t -> EConstr.types -> EConstr.typesval find_hnf_rectype : Environ.env -> Evd.evar_map -> EConstr.types -> (Names.inductive * EConstr.EInstance.t) * EConstr.constr listval contextually : bool -> (Locus.occurrences * Pattern.constr_pattern) -> (Ltac_pretype.patvar_map -> Reductionops.reduction_function) -> Reductionops.reduction_functionval e_contextually : bool -> (Locus.occurrences * Pattern.constr_pattern) -> (Ltac_pretype.patvar_map -> Reductionops.e_reduction_function) -> Reductionops.e_reduction_functionval check_privacy : Environ.env -> Names.inductive -> unitErrors if the inductive is not allowed for pattern-matching. *