G_redexprval int_or_var : int Locus.or_var Pcoq.Entry.tval nat_or_var : int Locus.or_var Pcoq.Entry.tval pattern_occ : Genredexpr.r_trm Locus.with_occurrences_expr Pcoq.Entry.tval unfold_occ : Genredexpr.r_cst Locus.with_occurrences_expr Pcoq.Entry.tval ref_or_pattern_occ : (Genredexpr.r_cst, Genredexpr.r_pat) Util.union Locus.with_occurrences_expr Pcoq.Entry.tval occs_nums : Locus.occurrences_expr Pcoq.Entry.tval occs : Locus.occurrences_expr Pcoq.Entry.tval delta_flag : Genredexpr.r_cst Genredexpr.red_atom Pcoq.Entry.tval strategy_flag : Genredexpr.r_cst Genredexpr.glob_red_flag Pcoq.Entry.t