Module `Tacred`Source

Sourcetype evaluable_global_reference =

| EvalVarRef of Names.Id.t
| EvalConstRef of Names.Constant.t

Sourceval eq_egr : evaluable_global_reference -> evaluable_global_reference -> bool

val subst_evaluable_reference : 
  Mod_subst.substitution ->
  evaluable_global_reference ->
  evaluable_global_reference

Here 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).

Sourcetype reduction_tactic_error =

| InvalidAbstraction of Environ.env * Evd.evar_map * EConstr.constr * Environ.env * Type_errors.type_error

Sourceexception ReductionTacticError of reduction_tactic_error

Reduction functions associated to tactics.

Evaluable global reference

Sourceval is_evaluable : Environ.env -> evaluable_global_reference -> bool

Sourceexception NotEvaluableRef of Names.GlobRef.t

Sourceval error_not_evaluable : Names.GlobRef.t -> 'a

Source

val evaluable_of_global_reference : 
  Environ.env ->
  Names.GlobRef.t ->
  evaluable_global_reference

Source

val global_of_evaluable_reference : 
  evaluable_global_reference ->
  Names.GlobRef.t

Source

val red_product : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr option

Red (returns None if nothing reducible)

Sourceval simpl : Reductionops.reduction_function

Simpl

Sourceval whd_simpl : Reductionops.reduction_function

Simpl only at the head

Sourceval 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

Sourceval hnf_constr0 : Reductionops.reduction_function

Variant of the above that does not perform nf-βι

Source

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

Unfold

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

Fold

Source

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

Pattern

Rem: Lazy strategies are defined in Reduction

Source

val cbv_norm_flags : 
  RedFlags.reds ->
  strong:bool ->
  Reductionops.reduction_function

Call by value strategy (uses Closures)

Sourceval cbv_beta : Reductionops.reduction_function

Sourceval cbv_betaiota : Reductionops.reduction_function

Sourceval cbv_betadeltaiota : Reductionops.reduction_function

Sourceval whd_compute : Reductionops.reduction_function

Sourceval compute : Reductionops.reduction_function

= cbv_betadeltaiota

Source

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

Source

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

Source

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

Same as reduce_to_quantified_ind but more efficient because it does not return the normalized type.

Source

val reduce_to_quantified_ref : 
  ?allow_failure:bool ->
  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). 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.

Source

val reduce_to_atomic_ref : 
  ?allow_failure:bool ->
  Environ.env ->
  Evd.evar_map ->
  Names.GlobRef.t ->
  EConstr.types ->
  EConstr.types

Source

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

Source

val contextually : 
  bool ->
  (Locus.occurrences * Pattern.constr_pattern) ->
  (Ltac_pretype.patvar_map -> Reductionops.reduction_function) ->
  Reductionops.reduction_function

Source

val e_contextually : 
  bool ->
  (Locus.occurrences * Pattern.constr_pattern) ->
  (Ltac_pretype.patvar_map -> Reductionops.e_reduction_function) ->
  Reductionops.e_reduction_function

Sourceval check_privacy : Environ.env -> Names.inductive -> unit

Errors if the inductive is not allowed for pattern-matching. *

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.pretyping/Tacred/index.html

Module `Tacred`Source

Reduction functions associated to tactics.

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.pretyping/Tacred/index.html

Module TacredSource

Reduction functions associated to tactics.

Module `Tacred`Source