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 ->
    Result.t Proofview.tactic) ->
  strategy