fix for bug #1347 (no more Scope pollution by FSets)

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

4 files changed, 9 insertions, 9 deletions

diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index d9abc7a0d..3cd6274cc 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -30,7 +30,7 @@ Module Raw (I:Int)(X: OrderedType).
 Import I.
 Module II:=MoreInt(I).
 Import II.
-Open Scope Int_scope.
+Open Local Scope Int_scope.
 
 Module E := X.
 Module MX := OrderedTypeFacts X.
@@ -1229,7 +1229,7 @@ Proof.
  apply compare_flatten_1.
 Qed.
 
-Open Scope Z_scope.
+Open Local Scope Z_scope.
 
 (** termination of [compare_aux] *)
  
@@ -1967,7 +1967,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
   Definition flatten_slist (e:enumeration D.t)(He:sorted_e e) := 
    LO.MapS.Build_slist (sorted_flatten_e He). 
 
-  Open Scope Z_scope.
+  Open Local Scope Z_scope.
 
   Definition compare_aux : 
    forall (e1 e2:enumeration D.t)(He1:sorted_e e1)(He2: sorted_e e2), 
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index 70c221027..af1e71de5 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -21,7 +21,7 @@ Require Import FMapInterface.
 
 Set Implicit Arguments.
 
-Open Scope positive_scope.
+Open Local Scope positive_scope.
 
 (** * An implementation of [FMapInterface.S] for positive keys. *)
 
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index 8bd51abec..f21ae6e8c 100644
--- a/theories/FSets/FSetAVL.v
+++ b/theories/FSets/FSetAVL.v
@@ -28,7 +28,7 @@ Module Raw (I:Int)(X:OrderedType).
 Import I.
 Module II:=MoreInt(I).
 Import II.
-Open Scope Int_scope.
+Open Local Scope Int_scope.
 
 Module E := X.
 Module MX := OrderedTypeFacts X.
@@ -2286,7 +2286,7 @@ Qed.
 
 (** termination of [compare_aux] *)
 
-Open Scope Z_scope.
+Open Local Scope Z_scope.
  
 Fixpoint measure_e_t (s : tree) : Z := match s with
   | Leaf => 0
diff --git a/theories/FSets/OrderedTypeEx.v b/theories/FSets/OrderedTypeEx.v
index b3227e5a8..1ed981f8d 100644
--- a/theories/FSets/OrderedTypeEx.v
+++ b/theories/FSets/OrderedTypeEx.v
@@ -73,7 +73,7 @@ End Nat_as_OT.
 
 (** [Z] is an ordered type with respect to the usual order on integers. *)
 
-Open Scope Z_scope.
+Open Local Scope Z_scope.
 
 Module Z_as_OT <: UsualOrderedType.
 
@@ -103,7 +103,7 @@ End Z_as_OT.
 
 (** [positive] is an ordered type with respect to the usual order on natural numbers. *) 
 
-Open Scope positive_scope.
+Open Local Scope positive_scope.
 
 Module Positive_as_OT <: UsualOrderedType.
   Definition t:=positive.
@@ -145,7 +145,7 @@ End Positive_as_OT.
 
 (** [N] is an ordered type with respect to the usual order on natural numbers. *) 
 
-Open Scope positive_scope.
+Open Local Scope positive_scope.
 
 Module N_as_OT <: UsualOrderedType.
   Definition t:=N.