From 813f6748aadc060b76e6c4c4484d8e0de48ff7a8 Mon Sep 17 00:00:00 2001
From: thery
Date: Thu, 12 Oct 2006 07:52:00 +0000
Subject: Fix name clash on left

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9234 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/setoid_ring/Field_theory.v | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/contrib/setoid_ring/Field_theory.v b/contrib/setoid_ring/Field_theory.v
index 206367ba2c..28f35c1a16 100644
--- a/contrib/setoid_ring/Field_theory.v
+++ b/contrib/setoid_ring/Field_theory.v
@@ -647,10 +647,14 @@ intros l e1 e2; elim e2; simpl; auto.
 Qed.
 
 Record rsplit : Type := mk_rsplit {
-   left : PExpr C;
-   common : PExpr C;
-   right : PExpr C}.
-
+   rsplit_left : PExpr C;
+   rsplit_common : PExpr C;
+   rsplit_right : PExpr C}.
+
+(* Stupid name clash *)
+Let left := rsplit_left.
+Let right := rsplit_right.
+Let common := rsplit_common.
 
 Fixpoint split (e1 e2: PExpr C) {struct e1}: rsplit :=
   match e1 with
-- 
cgit v1.2.3