aboutsummaryrefslogtreecommitdiffhomepage
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 c1d7f34ce..7c7362cad 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -284,7 +284,7 @@ Definition predicate_implication {l : list Type} :=
(** Notations for pointwise equivalence and implication of predicates. *)
Infix "<∙>" := predicate_equivalence (at level 95, no associativity) : predicate_scope.
-Infix "-∙>" := predicate_implication (at level 70) : predicate_scope.
+Infix "-∙>" := predicate_implication (at level 70, right associativity) : predicate_scope.
Open Local Scope predicate_scope.