diff options
| -rw-r--r-- | theories7/Reals/Rfunctions.v | 2 | ||||
| -rw-r--r-- | 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. |