From 509442d374432f3b49e77b0f90ff80519e1e4dfd Mon Sep 17 00:00:00 2001
From: desmettr
Date: Wed, 22 Jan 2003 14:14:12 +0000
Subject: Suppression d'un Import R_scope probablement oublie

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

diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v
index 0da625bab9..9331494271 100644
--- a/theories/Reals/R_sqr.v
+++ b/theories/Reals/R_sqr.v
@@ -168,7 +168,6 @@ Intros; Unfold Rsqr.
 Rewrite Rinv_Rmult; Try Reflexivity Orelse Assumption.
 Qed.
 
-Import R_scope.
 Lemma canonical_Rsqr : (a:nonzeroreal;b,c,x:R) ``a*(Rsqr x)+b*x+c == a* (Rsqr (x+b/(2*a))) + (4*a*c - (Rsqr b))/(4*a)``.
 Intros.
 Rewrite Rsqr_plus.
-- 
cgit v1.2.3