package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

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

Source

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

Source

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

Source

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

Source

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

Sourceval matches : Pattern.constr_pattern -> strategy

Sourceval ltac1_tactic_call : unit Proofview.tactic -> strategy

Source

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

package rocq-runtime

Module Rewrite.StrategiesSource

Module `Rewrite.Strategies`Source