package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
dune-project
Dependency
Authors
Maintainers
Sources
coq-8.19.2.tar.gz
md5=5d1187d5e44ed0163f76fb12dabf012e
sha512=91bc81530fa4f6498961583ad51eac5001f139881788b88e360a866ad8e2a6e2c5bce86d1a580ab4cd4782bf49d48318767df82471ce33ba3ac143e5569ad33c
doc/coq-core.tactics/Redexpr/index.html
Module RedexprSource
Interpretation layer of redexprs such as hnf, cbv, etc.
Source
val reduction_of_red_expr_val :
?occs:(Locus.occurrences_expr * int) ->
red_expr_val ->
Reductionops.e_reduction_function * Constr.cast_kindSource
val reduction_of_red_expr :
Environ.env ->
red_expr ->
Reductionops.e_reduction_function * Constr.cast_kindComposition of reduction_of_red_expr_val with eval_red_expr
true if we should use the vm to verify the reduction
Adding a custom reduction (function to be use at the ML level) NB: the effect is permanent.
Adding a custom reduction (function to be called a vernac command). The boolean flag is the locality.
Opaque and Transparent commands.
Source
val set_strategy :
bool ->
(Conv_oracle.level * Tacred.evaluable_global_reference list) list ->
unitSets the expansion strategy of a constant. When the boolean is true, the effect is non-synchronous (i.e. it does not survive section and module closure).
call by value normalisation function using the virtual machine
Source
val wit_red_expr :
((Constrexpr.constr_expr,
Libnames.qualid Constrexpr.or_by_notation,
Constrexpr.constr_expr)
Genredexpr.red_expr_gen,
(Genintern.glob_constr_and_expr,
Tacred.evaluable_global_reference Genredexpr.and_short_name Locus.or_var,
Genintern.glob_constr_pattern_and_expr)
Genredexpr.red_expr_gen,
(EConstr.t, Tacred.evaluable_global_reference, Pattern.constr_pattern)
Genredexpr.red_expr_gen)
Genarg.genarg_type