package rocq-runtime

  1. Overview
  2. Docs
package rocq-runtime
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Redexpr.UserSource

Sourcetype ('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;
}
Sourcetype ('raw, 'glb) user_red

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

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

Create a new user-defined reduction.

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

Inject the required data into a user reduction expression.