aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories7/Init
diff options
context:
space:
mode:
Diffstat (limited to 'theories7/Init')
-rw-r--r--theories7/Init/Notations.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories7/Init/Notations.v b/theories7/Init/Notations.v
index 624f6c902..fffdc5200 100644
--- a/theories7/Init/Notations.v
+++ b/theories7/Init/Notations.v
@@ -54,7 +54,7 @@ Uninterpreted Notation "x * y" (at level 3, right associativity)
Uninterpreted V8Notation "x / y" (at level 40, left associativity).
Uninterpreted V8Notation "- x" (at level 35, right associativity).
Uninterpreted V8Notation "/ x" (at level 35, right associativity).
-Uninterpreted V8Notation "x ^ y" (at level 30, left associativity).
+Uninterpreted V8Notation "x ^ y" (at level 30, right associativity).
(** Notations for pairs *)