diff options
| author | herbelin | 2006-10-26 18:25:06 +0000 |
|---|---|---|
| committer | herbelin | 2006-10-26 18:25:06 +0000 |
| commit | 48178a09bce619ba8aa74578debff9728e319c3b (patch) | |
| tree | d713c86ac974807c986defa86b158962b3c73979 | |
| parent | 7fec3599c078f23f105ab8ea32208a4720ffabaf (diff) | |
Noms de compatibilité déplacés en bloc à la fin du fichier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9288 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/field/LegacyField_Theory.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/contrib/field/LegacyField_Theory.v b/contrib/field/LegacyField_Theory.v index 5516f92fac..131ba84b83 100644 --- a/contrib/field/LegacyField_Theory.v +++ b/contrib/field/LegacyField_Theory.v @@ -102,8 +102,6 @@ Proof. intros; legacy ring. Qed. -Notation AplusT_sym := AplusT_comm (only parsing). (* Compatibility *) - Lemma AplusT_assoc : forall r1 r2 r3:AT, AplusT (AplusT r1 r2) r3 = AplusT r1 (AplusT r2 r3). Proof. @@ -115,8 +113,6 @@ Proof. intros; legacy ring. Qed. -Notation AmultT_sym := AmultT_comm (only parsing). (* Compatibility *) - Lemma AmultT_assoc : forall r1 r2 r3:AT, AmultT (AmultT r1 r2) r3 = AmultT r1 (AmultT r2 r3). Proof. @@ -648,3 +644,7 @@ unfold inverse_simplif in |- *; rewrite monom_simplif_correct; auto. Qed. End Theory_of_fields. + +(* Compatibility *) +Notation AplusT_sym := AplusT_comm (only parsing). +Notation AmultT_sym := AmultT_comm (only parsing). |