package rocq-runtime

  1. Overview
  2. Docs
package rocq-runtime
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module RewriteSource

TODO: document and clean me!

Sourcemodule Result : sig ... end
Sourcetype strategy
Sourceval cl_rewrite_clause_strat : strategy -> Names.Id.t option -> unit Proofview.tactic

Entry point for user-level "rewrite_strat"

Entry point for user-level "setoid_rewrite"

Sourceval is_applied_rewrite_relation : Environ.env -> Evd.evar_map -> EConstr.rel_context -> EConstr.constr -> EConstr.types option
Sourceval setoid_symmetry : unit Proofview.tactic
Sourceval setoid_symmetry_in : Names.Id.t -> unit Proofview.tactic
Sourceval setoid_reflexivity : unit Proofview.tactic
Sourceval setoid_transitivity : EConstr.constr option -> unit Proofview.tactic
Sourcemodule Strategies : sig ... end
Sourcemodule Internal : sig ... end