From e2f323f0d4e012618933d5fdb099ee44e4c0e7ac Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 13 May 2003 22:16:20 +0000
Subject: Notations arithmetiques

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4008 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/ring/ArithRing.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/contrib/ring/ArithRing.v b/contrib/ring/ArithRing.v
index e89017daf7..0a49ecb476 100644
--- a/contrib/ring/ArithRing.v
+++ b/contrib/ring/ArithRing.v
@@ -14,6 +14,9 @@ Require Export Ring.
 Require Export Arith.
 Require Eqdep_dec.
 
+V7only [Import nat_scope.].
+Open Local Scope nat_scope.
+
 Fixpoint nateq [n,m:nat] : bool :=
   Cases n m of
   | O O => true
-- 
cgit v1.2.3