From 2f2b225969cf4b06ff60d4a5862cf8404bb11268 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 9 Apr 2003 10:55:08 +0000
Subject: Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace
 "Import".
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

(limited to 'theories/ZArith/Zsqrt.v')

diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v
index a5ddfff4f..681dcdd12 100644
--- a/theories/ZArith/Zsqrt.v
+++ b/theories/ZArith/Zsqrt.v
@@ -11,7 +11,7 @@
 Require Export ZArith_base.
 Require Export ZArithRing.
 Require Export Omega.
-Import Z_scope.
+V7only [Import Z_scope.].
 
 (** The following tactic replaces all instances of (POS (xI ...)) by
     `2*(POS ...)+1` , but only when ... is not made only with xO, XI, or xH. *)
-- 
cgit v1.2.3