Up – Package index » rocq-runtime » Library rocq-runtime.tactics » Rewrite » Strategies

Module `Rewrite.Strategies`Source

Sourceval fail : strategy

Sourceval id : strategy

Sourceval refl : strategy

Sourceval progress : strategy -> strategy

Sourceval seq : strategy -> strategy -> strategy

Sourceval seqs : strategy list -> strategy

Sourceval choice : strategy -> strategy -> strategy

Sourceval choices : strategy list -> strategy

Sourceval try_ : strategy -> strategy

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

Sourceval fix : (strategy -> strategy) -> strategy

Sourceval any : strategy -> strategy

Sourceval repeat : strategy -> strategy

Sourceval all_subterms : strategy -> strategy

Sourceval one_subterm : strategy -> strategy

Sourceval bottomup : strategy -> strategy

Sourceval topdown : strategy -> strategy

Sourceval innermost : strategy -> strategy

Sourceval 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

Sourceval old_hints : string -> strategy

Sourceval hints : string -> strategy

Sourceval reduce : Redexpr.red_expr -> strategy

Sourceval fold : Evd.econstr -> strategy

Sourceval fold_glob : Glob_term.glob_constr -> strategy