package coq

  1. Overview
  2. Docs
Formal proof management system

Install 

dune-project
 Dependency

coq.inria.fr Edit opam file Versions (40)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors.

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.14.0.tar.gz
sha256=b1501d686c21836302191ae30f610cca57fb309214c126518ca009363ad2cd3c

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

Module TacredSource

Sourcetype evaluable_global_reference =
  1. | EvalVarRef of Names.Id.t
  2. | EvalConstRef of Names.Constant.t

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 =
  1. | 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
Sourceval error_not_evaluable : Names.GlobRef.t -> 'a
Sourceval evaluable_of_global_reference : Environ.env -> Names.GlobRef.t -> evaluable_global_reference
Sourceval global_of_evaluable_reference : evaluable_global_reference -> Names.GlobRef.t
Sourceexception Redelimination

Red (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

Unfold

Fold

Pattern

Rem: Lazy strategies are defined in Reduction

Call by value strategy (uses Closures)

= cbv_betadeltaiota

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

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

Sourceval 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

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

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