ComRewrite (coq-core.Ltac_plugin.ComRewrite)

type rewrite_attributes

val rewrite_attributes : rewrite_attributes Attributes.attribute

val declare_relation : rewrite_attributes -> ?binders:Constrexpr.local_binder_expr list ->
Constrexpr.constr_expr -> Constrexpr.constr_expr -> Names.Id.t -> Constrexpr.constr_expr option -> Constrexpr.constr_expr option -> Constrexpr.constr_expr option -> unit

val add_setoid : rewrite_attributes -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> Constrexpr.constr_expr -> Constrexpr.constr_expr -> Names.Id.t -> unit

val add_morphism_interactive : rewrite_attributes -> tactic:unit Proofview.tactic -> Constrexpr.constr_expr -> Names.Id.t -> Declare.Proof.t

val add_morphism_as_parameter : rewrite_attributes -> Constrexpr.constr_expr -> Names.Id.t -> unit

val add_morphism : rewrite_attributes -> tactic:unit Proofview.tactic -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> Constrexpr.constr_expr -> Names.Id.t -> Declare.Proof.t