*** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 0 deletions

diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index cda4273a5..455511633 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -15,6 +15,7 @@
 Require Export ZArith_base.
 Require Export Rsyntax.
 Require Export TypeSyntax.
+Import R_scope.
 
 (*********************************************************)
 (*               Field axioms                            *)
@@ -111,6 +112,8 @@ Fixpoint INR [n:nat]:R:=(Cases n of
                          |(S O)  => ``1``
                          |(S n)  => ``(INR n)+1``
                         end).  
+Arguments Scope INR [nat_scope].
+
 
 (**********************************************************) 
 (**      Injection from [Z] to [R]                        *)
@@ -122,6 +125,7 @@ Definition IZR:Z->R:=[z:Z](Cases z of
                         |(POS n) => (INR (convert n))
                         |(NEG n) => ``-(INR (convert n))``
                            end).  
+Arguments Scope IZR [Z_scope].
 
 (**********************************************************)
 (**      [R] Archimedian                                  *)