Strategies (rocq-runtime.Rewrite.Strategies)

val fail : strategy

val id : strategy

val refl : strategy

val progress : strategy -> strategy

val seq : strategy -> strategy -> strategy

val seqs : strategy list -> strategy

val choice : strategy -> strategy -> strategy

val choices : strategy list -> strategy

val try_ : strategy -> strategy

val fix_tac : (strategy -> strategy Proofview.tactic) -> strategy Proofview.tactic

val fix : (strategy -> strategy) -> strategy

val any : strategy -> strategy

val repeat : strategy -> strategy

val all_subterms : strategy -> strategy

val one_subterm : strategy -> strategy

val bottomup : strategy -> strategy

val topdown : strategy -> strategy

val innermost : strategy -> strategy

val outermost : strategy -> strategy

val one_lemma : Tactypes.delayed_open_constr -> bool -> Gentactic.glob_generic_tactic option -> Locus.occurrences -> strategy

val lemmas : (Tactypes.delayed_open_constr * bool * Gentactic.glob_generic_tactic option) list -> strategy

val old_hints : string -> strategy

val hints : string -> strategy

val reduce : Redexpr.red_expr -> strategy

val fold : Evd.econstr -> strategy

val fold_glob : Glob_term.glob_constr -> strategy

val with_env : (Environ.env -> Evd.evar_map -> Evd.evar_map * strategy) -> strategy

val matches : Pattern.constr_pattern -> strategy

val ltac1_tactic_call : unit Proofview.tactic -> strategy

val tactic_call : (env:Environ.env -> carrier:EConstr.constr -> lhs:EConstr.constr -> rel:EConstr.constr option -> rewrite_result Proofview.tactic) -> strategy