aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init/Notations.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Init/Notations.v')
-rw-r--r--theories/Init/Notations.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index ce1d4d7c9..05bfae722 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -47,7 +47,7 @@ Reserved Notation "x * y" (at level 40, left associativity).
Reserved Notation "x / y" (at level 40, left associativity).
Reserved Notation "- x" (at level 35, right associativity).
Reserved Notation "/ x" (at level 35, right associativity).
-Reserved Notation "x ^ y" (at level 30, left associativity).
+Reserved Notation "x ^ y" (at level 30, right associativity).
(** Notations for pairs *)