From eb2f9b5023f6d42f89ddfb3927fda81d6cb334a1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 9 Jan 2004 14:42:52 +0000
Subject: Retrait de la notation '^' pour 'power' en V7 car sinon confusion
 avec la syntaxe '^' de append qui est a un autre niveau

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5188 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories7/Reals/Rfunctions.v | 2 +-
 theories7/ZArith/Zpower.v    | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories7/Reals/Rfunctions.v b/theories7/Reals/Rfunctions.v
index b283b9fd8e..1cc3275374 100644
--- a/theories7/Reals/Rfunctions.v
+++ b/theories7/Reals/Rfunctions.v
@@ -70,7 +70,7 @@ Fixpoint pow [r:R;n:nat]:R:=
     |(S n) => (Rmult r (pow r n))
   end.
 
-Infix "^" pow (at level 2, left associativity) : R_scope V8only.
+V8Infix "^" pow : R_scope.
 
 Lemma pow_O: (x : R)  (pow x O) == R1.
 Proof.
diff --git a/theories7/ZArith/Zpower.v b/theories7/ZArith/Zpower.v
index 73e8a08da3..dbfdf22293 100644
--- a/theories7/ZArith/Zpower.v
+++ b/theories7/ZArith/Zpower.v
@@ -73,7 +73,7 @@ Definition Zpower :=
   | (NEG p) => `0`
   end.
 
-Infix "^" Zpower (at level 2, left associativity) : Z_scope V8only.
+V8Infix "^" Zpower : Z_scope.
 
 Hints Immediate Zpower_nat_is_exp : zarith.
 Hints Immediate Zpower_pos_is_exp : zarith.
@@ -93,7 +93,7 @@ End section1.
 
 (* Exporting notation "^" *)
 
-Infix "^" Zpower (at level 2, left associativity) : Z_scope V8only.
+V8Infix "^" Zpower : Z_scope.
 
 Hints Immediate Zpower_nat_is_exp : zarith.
 Hints Immediate Zpower_pos_is_exp : zarith.
-- 
cgit v1.2.3