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

6 files changed, 51 insertions, 42 deletions

diff --git a/contrib/correctness/Sorted.v b/contrib/correctness/Sorted.v
index 73179ed1e..8c3743a1e 100644
--- a/contrib/correctness/Sorted.v
+++ b/contrib/correctness/Sorted.v
@@ -15,7 +15,7 @@ Require ArrayPermut.
 
 Require ZArithRing.
 Require Omega.
-Import Z_scope.
+V7only [Import Z_scope.].
 
 Set Implicit Arguments.
 
diff --git a/contrib/omega/Omega.v b/contrib/omega/Omega.v
index 84ede032b..70ede13d0 100755
--- a/contrib/omega/Omega.v
+++ b/contrib/omega/Omega.v
@@ -30,8 +30,10 @@ Hints Resolve Zle_n Zplus_sym Zplus_assoc Zmult_sym Zmult_assoc
 
 Require Export Zhints.
 
+(*
 (* The constant minus is required in coq_omega.ml *)
-Require Export Minus.
+Require Minus.
+*)
 
 Hint eq_nat_Omega : zarith := Extern 10 (eq nat ? ?) Abstract Omega.
 Hint le_Omega : zarith := Extern 10 (le ? ?) Abstract Omega.
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.
diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v
index 8b209bde2..b08ef8272 100644
--- a/theories/Reals/Rsyntax.v
+++ b/theories/Reals/Rsyntax.v
@@ -197,12 +197,9 @@ Syntax constr
 .
 ].
 (* For parsing/printing based on scopes *)
+V7only [
 Module R_scope.
-
-Delimits Scope R_scope with R.
-
-(* Warning: this hides sum and prod and breaks sumor symbolic notation *)
-Open Scope R_scope.
+].
 
 Infix "<=" Rle (at level 5, no associativity) : R_scope.
 Infix "<"  Rlt (at level 5, no associativity) : R_scope.
@@ -237,4 +234,10 @@ Notation "x <> y" := ~(eqT R x y) (at level 5) : R_scope.
 Notation "/ x" := (Rinv x) (at level 0): R_scope
   V8only (at level 30, left associativity).
 
+V7only [
+Open Scope R_scope.
 End R_scope.
+].
+
+Delimits Scope R_scope with R.
+
diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v
index 81c0d9817..757b539ab 100644
--- a/theories/ZArith/Zsyntax.v
+++ b/theories/ZArith/Zsyntax.v
@@ -221,18 +221,9 @@ Syntax constr
 ].
 
 (* For parsing/printing based on scopes *)
+V7only [
 Module Z_scope.
-
-(* Declare Scope positive_scope with Key P. *)
-
-Delimits Scope positive_scope with P.
-Delimits Scope Z_scope with Z.
-
-(* Warning: this hides sum and prod and breaks sumor symbolic notation *)
-Open Scope Z_scope.
-
-Arguments Scope POS [positive_scope].
-Arguments Scope NEG [positive_scope].
+].
 
 Infix LEFTA 4 "+" Zplus : Z_scope.
 Infix LEFTA 4 "-" Zminus : Z_scope.
@@ -272,4 +263,16 @@ Syntax constr level 0:
   Zeq [ (eq Z $n1 $n2) ] -> [[<hov 0> $n1 [1 0] "= " $n2 ]].
 ].
 
+V7only [
+Open Scope Z_scope.
 End Z_scope.
+].
+
+(* Declare Scope positive_scope with Key P. *)
+
+Delimits Scope positive_scope with P.
+Delimits Scope Z_scope with Z.
+
+Arguments Scope POS [positive_scope].
+Arguments Scope NEG [positive_scope].
+