Module Genredexpr

Reduction expressions

type 'a red_atom =
| FBeta
| FMatch
| FFix
| FCofix
| FZeta
| FConst of 'a list
| FDeltaBut of 'a list
type 'a glob_red_flag = {
rBeta : bool;
rMatch : bool;
rFix : bool;
rCofix : bool;
rZeta : bool;
rDelta : bool;

true = delta all but rConst; false = delta only on rConst

rConst : 'a list;
}
type ('a, 'b, 'c) red_expr_gen =
| Red of bool
| Hnf
| Simpl of 'b glob_red_flag * ('b, 'c) Util.union Locus.with_occurrences option
| Cbv of 'b glob_red_flag
| Cbn of 'b glob_red_flag
| Lazy of 'b glob_red_flag
| Unfold of 'b Locus.with_occurrences list
| Fold of 'a list
| Pattern of 'a Locus.with_occurrences list
| ExtraRedExpr of string
| CbvVm of ('b, 'c) Util.union Locus.with_occurrences option
| CbvNative of ('b, 'c) Util.union Locus.with_occurrences option
type ('a, 'b, 'c) may_eval =
| ConstrTerm of 'a
| ConstrEval of ('a, 'b, 'c) red_expr_gen * 'a
| ConstrContext of Names.lident * 'a
| ConstrTypeOf of 'a
type r_trm = Constrexpr.constr_expr
type r_pat = Constrexpr.constr_pattern_expr
type r_cst = Libnames.qualid Constrexpr.or_by_notation
type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
val make0 : ?⁠dyn:'a Geninterp.Val.tag -> string -> ('b, 'c, 'a) Genarg.genarg_type
type 'a and_short_name = 'a * Names.lident option
val wit_red_expr : ((Constrexpr.constr_expr, Libnames.qualid Constrexpr.or_by_notation, Constrexpr.constr_expr) red_expr_gen, (Genintern.glob_constr_and_expr, Names.evaluable_global_reference and_short_name Locus.or_var, Genintern.glob_constr_pattern_and_expr) red_expr_gen, (EConstr.t, Names.evaluable_global_reference, Pattern.constr_pattern) red_expr_gen) Genarg.genarg_type