package coq-core
Install
Dune Dependency
Authors
Maintainers
Sources
md5=8d852367b54f095d9fbabd000304d450
sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50
doc/coq-core.pretyping/Tacred/index.html
Module TacredSource
type evaluable_global_reference = | EvalVarRef of Names.Id.t| EvalConstRef of Names.Constant.t
val 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
Reduction functions associated to tactics.
Evaluable global reference
val evaluable_of_global_reference :
Environ.env ->
Names.GlobRef.t ->
evaluable_global_referenceRed (raise user error if nothing reducible)
Red (raise Redelimination if nothing reducible)
Simpl
Simpl only at the head
Hnf: like whd_simpl but force delta-reduction of constants that do not immediately hide a non reducible fix or cofix
Variant of the above that does not perform nf-βι
val unfoldn :
(Locus.occurrences * evaluable_global_reference) list ->
Reductionops.reduction_functionUnfold
Fold
val pattern_occs :
(Locus.occurrences * EConstr.constr) list ->
Reductionops.e_reduction_functionPattern
Rem: Lazy strategies are defined in Reduction
Call by value strategy (uses Closures)
= 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_functionErrors if the inductive is not allowed for pattern-matching. *