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