From 86fb851af84e7e62d7f8e3825e78d3ad38bbbdfe Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 12 Sep 2003 14:42:11 +0000
Subject: Bind et Delimit pour R

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

diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v
index 620400d614..26857c81f1 100644
--- a/theories/Reals/Rdefinitions.v
+++ b/theories/Reals/Rdefinitions.v
@@ -17,6 +17,10 @@ Require Export ZArith_base.
 Require Export TypeSyntax.
 
 Parameter R:Type.
+
+Delimits Scope R_scope with R.
+Bind Scope R_scope with R.
+
 Parameter R0:R.
 Parameter R1:R.
 Parameter Rplus:R->R->R.
-- 
cgit v1.2.3