Ltac_plugin.ComRewriteval rewrite_attributes : rewrite_attributes Attributes.attributeval 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 -> unitval add_setoid : rewrite_attributes -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> Constrexpr.constr_expr -> Constrexpr.constr_expr -> Names.Id.t -> unitval add_morphism_interactive : rewrite_attributes -> tactic:unit Proofview.tactic -> Constrexpr.constr_expr -> Names.Id.t -> Declare.Proof.tval add_morphism_as_parameter : rewrite_attributes -> Constrexpr.constr_expr -> Names.Id.t -> unitval 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