Encore des _sym au lieu de _comm

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

5 files changed, 7 insertions, 7 deletions

diff --git a/contrib/ring/LegacyRing_theory.v b/contrib/ring/LegacyRing_theory.v
index 192ff1f57..79f6976bd 100644
--- a/contrib/ring/LegacyRing_theory.v
+++ b/contrib/ring/LegacyRing_theory.v
@@ -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. 
diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v
index 28de54e65..9b85fb85e 100644
--- a/contrib/ring/Ring_abstract.v
+++ b/contrib/ring/Ring_abstract.v
@@ -428,7 +428,7 @@ Fixpoint interp_ap (p:apolynomial) : A :=
 Hint Resolve (Th_plus_comm T).
 Hint Resolve (Th_plus_assoc T).
 Hint Resolve (Th_plus_assoc2 T).
-Hint Resolve (Th_mult_sym T).
+Hint Resolve (Th_mult_comm T).
 Hint Resolve (Th_mult_assoc T).
 Hint Resolve (Th_mult_assoc2 T).
 Hint Resolve (Th_plus_zero_left T).
diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v
index 199ae7572..4f2426337 100644
--- a/contrib/ring/Ring_normalize.v
+++ b/contrib/ring/Ring_normalize.v
@@ -774,7 +774,7 @@ Variable T : Ring_Theory Aplus Amult Aone Azero Aopp Aeq.
 Hint Resolve (Th_plus_comm T).
 Hint Resolve (Th_plus_assoc T).
 Hint Resolve (Th_plus_assoc2 T).
-Hint Resolve (Th_mult_sym T).
+Hint Resolve (Th_mult_comm T).
 Hint Resolve (Th_mult_assoc T).
 Hint Resolve (Th_mult_assoc2 T).
 Hint Resolve (Th_plus_zero_left T).
diff --git a/contrib/ring/Setoid_ring_normalize.v b/contrib/ring/Setoid_ring_normalize.v
index 96ba632fc..ce23d05af 100644
--- a/contrib/ring/Setoid_ring_normalize.v
+++ b/contrib/ring/Setoid_ring_normalize.v
@@ -1032,7 +1032,7 @@ Variable T : Setoid_Ring_Theory Aequiv Aplus Amult Aone Azero Aopp Aeq.
 Hint Resolve (STh_plus_comm T).
 Hint Resolve (STh_plus_assoc T).
 Hint Resolve (STh_plus_assoc2 S T).
-Hint Resolve (STh_mult_sym T).
+Hint Resolve (STh_mult_comm T).
 Hint Resolve (STh_mult_assoc T).
 Hint Resolve (STh_mult_assoc2 S T).
 Hint Resolve (STh_plus_zero_left T).
diff --git a/contrib/ring/Setoid_ring_theory.v b/contrib/ring/Setoid_ring_theory.v
index ff18e7b35..4ec8433fe 100644
--- a/contrib/ring/Setoid_ring_theory.v
+++ b/contrib/ring/Setoid_ring_theory.v
@@ -177,7 +177,7 @@ Section Theory_of_setoid_rings.
 Record Setoid_Ring_Theory : Prop := 
   {STh_plus_comm : forall n m:A, n + m == m + n;
    STh_plus_assoc : forall n m p:A, n + (m + p) == n + m + p;
-   STh_mult_sym : forall n m:A, n * m == m * n;
+   STh_mult_comm : forall n m:A, n * m == m * n;
    STh_mult_assoc : forall n m p:A, n * (m * p) == n * m * p;
    STh_plus_zero_left : forall n:A, 0 + n == n;
    STh_mult_one_left : forall n:A, 1 * n == n;
@@ -189,7 +189,7 @@ Variable T : Setoid_Ring_Theory.
 
 Let plus_comm := STh_plus_comm T.
 Let plus_assoc := STh_plus_assoc T.
-Let mult_comm := STh_mult_sym T.
+Let mult_comm := STh_mult_comm T.
 Let mult_assoc := STh_mult_assoc T.
 Let plus_zero_left := STh_plus_zero_left T.
 Let mult_one_left := STh_mult_one_left T.