G_redexpr (u.4b72d9d53197f808b005effa2cda4f29.coq-core.8.20.1.doc.coq-core.vernac.G

Sourceval int_or_var : int Locus.or_var Pcoq.Entry.t

Sourceval nat_or_var : int Locus.or_var Pcoq.Entry.t

Sourceval pattern_occ : Genredexpr.r_trm Locus.with_occurrences_expr Pcoq.Entry.t

Sourceval unfold_occ : Genredexpr.r_cst Locus.with_occurrences_expr Pcoq.Entry.t

val ref_or_pattern_occ : 
  (Genredexpr.r_cst, Genredexpr.r_pat) Util.union Locus.with_occurrences_expr
    Pcoq.Entry.t

Sourceval occs_nums : Locus.occurrences_expr Pcoq.Entry.t

Sourceval occs : Locus.occurrences_expr Pcoq.Entry.t

Sourceval delta_flag : Genredexpr.r_cst Genredexpr.red_atom Pcoq.Entry.t

Sourceval strategy_flag : Genredexpr.r_cst Genredexpr.glob_red_flag Pcoq.Entry.t