power associe a droite

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5072 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 6 insertions, 6 deletions

diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index ce1d4d7c9a..05bfae722e 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 *)
 
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 30b4a5396e..62eff1d1f3 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -419,7 +419,7 @@ rewrite Hrecn; rewrite Rmult_1_l; simpl in |- *; rewrite Rmult_1_r;
  rewrite Rabs_Ropp; apply Rabs_R1.
 Qed.
 
-Lemma pow_mult : forall (x:R) (n1 n2:nat), x ^ (n1 * n2) = x ^ n1 ^ n2.
+Lemma pow_mult : forall (x:R) (n1 n2:nat), x ^ (n1 * n2) = (x ^ n1) ^ n2.
 Proof.
 intros; induction  n2 as [| n2 Hrecn2].
 simpl in |- *; replace (n1 * 0)%nat with 0%nat; [ reflexivity | ring ].
@@ -534,7 +534,7 @@ Definition powerRZ (x:R) (n:Z) :=
   | Zneg p => / x ^ nat_of_P p
   end.
 
-Infix Local "^Z" := powerRZ (at level 30, left associativity) : R_scope.
+Infix Local "^Z" := powerRZ (at level 30, right associativity) : R_scope.
 
 Lemma Zpower_NR0 :
  forall (x:Z) (n:nat), (0 <= x)%Z -> (0 <= Zpower_nat x n)%Z.
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v
index 7c31bbe613..30f7be1f03 100644
--- a/theories/Reals/Rpower.v
+++ b/theories/Reals/Rpower.v
@@ -379,7 +379,7 @@ Qed.
  
 Definition Rpower (x y:R) := exp (y * ln x).
 
-Infix Local "^R" := Rpower (at level 30, left associativity) : R_scope.
+Infix Local "^R" := Rpower (at level 30, right associativity) : R_scope.
 
 (******************************************************************)
 (*                        Properties of  Rpower                   *)
@@ -390,7 +390,7 @@ intros x y z; unfold Rpower in |- *.
 rewrite Rmult_plus_distr_r; rewrite exp_plus; auto.
 Qed.
  
-Theorem Rpower_mult : forall x y z:R, x ^R y ^R z = x ^R (y * z).
+Theorem Rpower_mult : forall x y z:R, (x ^R y) ^R z = x ^R (y * z).
 intros x y z; unfold Rpower in |- *.
 rewrite ln_exp.
 replace (z * (y * ln x)) with (y * z * ln x).
@@ -437,7 +437,7 @@ apply sqrt_lt_R0; apply H.
 apply Rmult_eq_reg_l with (INR 2).
 apply exp_inv.
 fold Rpower in |- *.
-cut (x ^R (/ 2) ^R INR 2 = sqrt x ^R INR 2).
+cut ((x ^R (/ 2)) ^R INR 2 = sqrt x ^R INR 2).
 unfold Rpower in |- *; auto.
 rewrite Rpower_mult.
 rewrite Rinv_l.