Module `Redexpr`Source

Interpretation layer of redexprs such as hnf, cbv, etc.

type red_expr =
  (EConstr.constr, Evaluable.t, Pattern.constr_pattern, int)
    Genredexpr.red_expr_gen

Sourcetype red_expr_val

Sourceval out_occurrences : Locus.occurrences_expr -> Locus.occurrences

Source

val out_with_occurrences : 
  'a Locus.with_occurrences_expr ->
  'a Locus.with_occurrences

Sourceval eval_red_expr : Environ.env -> red_expr -> red_expr_val

Source

val reduction_of_red_expr_val : 
  ?occs:(Locus.occurrences * int) ->
  red_expr_val ->
  Reductionops.e_reduction_function * Constr.cast_kind

Source

val reduction_of_red_expr : 
  Environ.env ->
  red_expr ->
  Reductionops.e_reduction_function * Constr.cast_kind

Composition of reduction_of_red_expr_val with eval_red_expr

true if we should use the vm to verify the reduction

Sourceval declare_reduction : string -> Reductionops.reduction_function -> unit

Adding a custom reduction (function to be use at the ML level) NB: the effect is permanent.

Sourceval declare_red_expr : bool -> string -> red_expr -> unit

Adding a custom reduction (function to be called a vernac command). The boolean flag is the locality.

Opaque and Transparent commands.

Sourceval set_strategy : bool -> (Conv_oracle.level * Evaluable.t list) list -> unit

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

Sourceval cbv_vm : Reductionops.reduction_function

call by value normalisation function using the virtual machine

Sourceval subst_red_expr : Mod_subst.substitution -> red_expr -> red_expr

subst_red_expr sub c performs the substitution sub on all kernel names appearing in c

Source

val wit_red_expr : 
  (Genredexpr.raw_red_expr, Genredexpr.glob_red_expr, red_expr)
    Genarg.genarg_type

Sourcemodule Intern : sig ... end

Sourcemodule Interp : sig ... end

Source

val interp_redexp_no_ltac : 
  Environ.env ->
  Evd.evar_map ->
  Genredexpr.raw_red_expr ->
  Evd.evar_map * red_expr

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.tactics/Redexpr/index.html

Module `Redexpr`Source

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.tactics/Redexpr/index.html

Module RedexprSource

Module `Redexpr`Source