Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

1 files changed, 3 insertions, 3 deletions

diff --git a/contrib/ring/LegacyRing_theory.v b/contrib/ring/LegacyRing_theory.v
index 5df927a6..d15d18a6 100644
--- a/contrib/ring/LegacyRing_theory.v
+++ b/contrib/ring/LegacyRing_theory.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: LegacyRing_theory.v 9179 2006-09-26 12:13:06Z barras $ *)
+(* $Id: LegacyRing_theory.v 9370 2006-11-13 09:21:31Z herbelin $ *)
 
 Require Export Bool.
 
@@ -153,7 +153,7 @@ Notation "- x" := (Aopp x).
 Record Ring_Theory : Prop := 
   {Th_plus_comm : forall n m:A, n + m = m + n;
    Th_plus_assoc : forall n m p:A, n + (m + p) = n + m + p;
-   Th_mult_sym : forall n m:A, n * m = m * n;
+   Th_mult_comm : forall n m:A, n * m = m * n;
    Th_mult_assoc : forall n m p:A, n * (m * p) = n * m * p;
    Th_plus_zero_left : forall n:A, 0 + n = n;
    Th_mult_one_left : forall n:A, 1 * n = n;
@@ -165,7 +165,7 @@ Variable T : Ring_Theory.
 
 Let plus_comm := Th_plus_comm T.
 Let plus_assoc := Th_plus_assoc T.
-Let mult_comm := Th_mult_sym T.
+Let mult_comm := Th_mult_comm T.
 Let mult_assoc := Th_mult_assoc T.
 Let plus_zero_left := Th_plus_zero_left T.
 Let mult_one_left := Th_mult_one_left T.