package coq
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=3cbfc1e1a72b16d4744f5b64ede59586071e31d9c11c811a0372060727bfd9c3
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
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 reduce_to_quantified_ref :
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) and fails with user error if not possible
val reduce_to_atomic_ref :
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 Univ.puniverses ->
Names.inductive Univ.puniversesReturns 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.puniversesReturns the same inductive if it is not a primitive record raises an error otherwise. *