Module Redexpr.User

type ('raw, 'glb) user_red_spec = {
  1. ured_intern : Constrintern.ltac_sign -> 'raw -> 'glb;
  2. ured_subst : Mod_subst.substitution -> 'glb -> 'glb;
  3. ured_eval : 'glb -> Reductionops.e_reduction_function * Constr.cast_kind;
  4. ured_rprint : Environ.env -> Evd.evar_map -> 'raw -> Pp.t;
  5. ured_gprint : Environ.env -> Evd.evar_map -> 'glb -> Pp.t;
}
type ('raw, 'glb) user_red

User-defined reductions are indexed by the kind of payload they contain at both raw and glob levels.

val create : string -> ('raw, 'glb) user_red_spec -> ('raw, 'glb) user_red

Create a new user-defined reduction.

val make : ('raw, 'glb) user_red -> 'raw -> Genarg.rlevel user_red_expr

Inject the required data into a user reduction expression.