Rewrite.Strategiesval fail : strategyval id : strategyval refl : strategyval fix_tac : (strategy -> strategy Proofview.tactic) -> strategy Proofview.tacticval one_lemma : Tactypes.delayed_open_constr -> bool -> Gentactic.glob_generic_tactic option -> Locus.occurrences -> strategyval lemmas : (Tactypes.delayed_open_constr * bool * Gentactic.glob_generic_tactic option) list -> strategyval old_hints : string -> strategyval hints : string -> strategyval reduce : Redexpr.red_expr -> strategyval fold : Evd.econstr -> strategyval fold_glob : Glob_term.glob_constr -> strategy