aboutsummaryrefslogtreecommitdiff
path: root/theories/Classes/RelationClasses.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Classes/RelationClasses.v')
-rw-r--r--theories/Classes/RelationClasses.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 36c328cf4d..b8fdac8c9d 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -56,7 +56,7 @@ Class Asymmetric {A} (R : relation A) :=
Class Transitive {A} (R : relation A) :=
transitivity : forall x y z, R x y -> R y z -> R x z.
-Hint Resolve @irreflexivity : ord.
+Hint Resolve irreflexivity : ord.
Unset Implicit Arguments.