Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"

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

2 files changed, 25 insertions, 24 deletions

diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index a3774efb6..0cb7edd7f 100755
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -174,3 +174,28 @@ Proof.
   Induction n; Auto.
   Induction m; Auto.
 Qed.
+
+(** Notations *)
+V7only[
+Syntax constr
+  level 0:
+    S [ (S $p) ] -> [$p:"nat_printer":9]
+  | O [ O ]      -> ["(0)"].
+].
+V7only [
+Module nat_scope.
+].
+
+(* For parsing/printing based on scopes *)
+Infix 4 "+" plus : nat_scope V8only (left associativity).
+Infix 4 "-" minus : nat_scope V8only (left associativity).
+Infix 3 "*" mult : nat_scope V8only (left associativity).
+Infix NONA 5 "<=" le : nat_scope.
+Infix NONA 5 "<" lt : nat_scope.
+Infix NONA 5 ">=" ge : nat_scope.
+Infix NONA 5 ">" gt : nat_scope.
+
+V7only [
+End nat_scope.
+].
+Delimits Scope nat_scope with N.
diff --git a/theories/Init/PeanoSyntax.v b/theories/Init/PeanoSyntax.v
index 072be35dd..3b7b91454 100644
--- a/theories/Init/PeanoSyntax.v
+++ b/theories/Init/PeanoSyntax.v
@@ -10,27 +10,3 @@
 Require Datatypes.
 Require Peano.
 
-V7only[
-Syntax constr
-  level 0:
-    S [ (S $p) ] -> [$p:"nat_printer":9]
-  | O [ O ]      -> ["(0)"].
-].
-(* Outside the module to be able to parse the grammar for 0,1,2... !! *)
-Delimits Scope nat_scope with N.
-
-(* For parsing/printing based on scopes *)
-Module nat_scope.
-
-(* Warning: this hides sum and prod and breaks sumor symbolic notation *)
-Open Scope nat_scope.
-
-Infix 4 "+" plus : nat_scope V8only (left associativity).
-Infix 4 "-" minus : nat_scope V8only (left associativity).
-Infix 3 "*" mult : nat_scope V8only (left associativity).
-Infix NONA 5 "<=" le : nat_scope.
-Infix NONA 5 "<" lt : nat_scope.
-Infix NONA 5 ">=" ge : nat_scope.
-Infix NONA 5 ">" gt : nat_scope.
-
-End nat_scope.