From 48178a09bce619ba8aa74578debff9728e319c3b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 26 Oct 2006 18:25:06 +0000
Subject: 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
---
 contrib/field/LegacyField_Theory.v | 8 ++++----
 1 file 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).
-- 
cgit v1.2.3