Redexpr (p.coq-core.8.18.0.doc.coq-core.tactics.Redexpr)

Source

type red_expr =
  (EConstr.constr, Tacred.evaluable_global_reference, Pattern.constr_pattern)
    Genredexpr.red_expr_gen

Sourcetype red_expr_val

Sourceval out_with_occurrences : 'a Locus.with_occurrences -> Locus.occurrences * 'a

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

Source

val reduction_of_red_expr_val : 
  ?occs:(Locus.occurrences_expr * 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.

Source

val set_strategy : 
  bool ->
  (Conv_oracle.level * Tacred.evaluable_global_reference 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

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