aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Classes/SetoidTactics.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Classes/SetoidTactics.v')
-rw-r--r--theories/Classes/SetoidTactics.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index ff5f7cb6c..e939d3ee7 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -38,7 +38,7 @@ Definition default_relation [ DefaultRelation A R ] := R.
(** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *)
-Instance equivalence_default [ Equivalence A R ] : DefaultRelation A R | 4.
+Instance equivalence_default [ Equivalence A R ] : DefaultRelation R | 4.
(** The setoid_replace tactics in Ltac, defined in terms of default relations and
the setoid_rewrite tactic. *)