power associe a droite

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

5 files changed, 10 insertions, 10 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index ea1c889586..72cf9d6348 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -2375,7 +2375,7 @@ let main files =
 		       "Scheme new_scheme := Induction for _ Sort _
 with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 
-  (* Template for Cases *)
+  (* Template for match *)
   let callback = (fun () -> 
 		    let w = get_current_word () in
 		    try 
@@ -2389,7 +2389,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 		      in
 		      let b = Buffer.create 1024 in
 		      let fmt = formatter_of_buffer b in
-		      fprintf fmt "@[Cases var of@\n%aend@]@."
+		      fprintf fmt "@[match var with@\n%aend@]@."
 			(print_list print) cases;
 		      let s = Buffer.contents b in
 		      prerr_endline s;
@@ -2407,7 +2407,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 		    with Not_found -> !flash_info "Not an inductive type"
 		 )
   in
-  ignore (templates_factory#add_item "Cases ..."
+  ignore (templates_factory#add_item "match ..."
 	    ~key:GdkKeysyms._C
 	    ~callback
 	 );
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.
diff --git a/theories7/Init/Notations.v b/theories7/Init/Notations.v
index 624f6c9025..fffdc52004 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 *)