aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init/Notations.v
diff options
context:
space:
mode:
authorGravatar marche <marche@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-12-05 16:42:46 +0000
committerGravatar marche <marche@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-12-05 16:42:46 +0000
commit7095630625a8f9657f681c488514f589ea63334e (patch)
tree19a41077333781f368375c5b9fc11e2a2a956f20 /theories/Init/Notations.v
parentaae1ebe54ab2ea42111e4c429d96129ce176acf5 (diff)
power associe a droite
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5072 85f007b7-540e-0410-9357-904b9bb8a0f7
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 *)