From 3fd4c212e742169b80ac709a6a7f68a47eff61b1 Mon Sep 17 00:00:00 2001
From: barras
Date: Mon, 30 Oct 2006 10:26:46 +0000
Subject: LegacyRfield was opening R_scope

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9317 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/LegacyRfield.v | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/theories/Reals/LegacyRfield.v b/theories/Reals/LegacyRfield.v
index d285fef30e..b33274af92 100644
--- a/theories/Reals/LegacyRfield.v
+++ b/theories/Reals/LegacyRfield.v
@@ -11,6 +11,9 @@
 Require Export Raxioms.
 Require Export LegacyField.
 Import LegacyRing_theory.
+
+Section LegacyRfield.
+
 Open Scope R_scope.
 
 Lemma RLegacyTheory : Ring_Theory Rplus Rmult 1 0 Ropp (fun x y:R => false).
@@ -30,6 +33,8 @@ Lemma RLegacyTheory : Ring_Theory Rplus Rmult 1 0 Ropp (fun x y:R => false).
   intros; contradiction.
 Defined.
 
+End LegacyRfield.
+
 Add Legacy Field
-R Rplus Rmult 1 0 Ropp (fun x y:R => false) Rinv RLegacyTheory Rinv_l
+R Rplus Rmult 1%R 0%R Ropp (fun x y:R => false) Rinv RLegacyTheory Rinv_l
   with minus := Rminus div := Rdiv.
-- 
cgit v1.2.3