4 files changed, 14 insertions, 14 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 786ade0e..4807ed66 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -9,7 +9,7 @@
 
 (* Finite map library.  *)
 
-(* $Id: FMapAVL.v 8985 2006-06-23 16:12:45Z jforest $ *)
+(* $Id: FMapAVL.v 9862 2007-05-25 16:57:06Z letouzey $ *)
 
 (** This module implements map using AVL trees.
     It follows the implementation from Ocaml's standard library. *)
@@ -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 911de00e..44724767 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -11,7 +11,7 @@
  * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
  *              91405 Orsay, France *)
 
-(* $Id: FMapPositive.v 9178 2006-09-26 11:18:22Z barras $ *)
+(* $Id: FMapPositive.v 9862 2007-05-25 16:57:06Z letouzey $ *)
 
 Require Import Bool.
 Require Import ZArith.
@@ -20,7 +20,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 5b09945b..d5ce54d9 100644
--- a/theories/FSets/FSetAVL.v
+++ b/theories/FSets/FSetAVL.v
@@ -12,7 +12,7 @@
  * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
  *              91405 Orsay, France *)
 
-(* $Id: FSetAVL.v 8985 2006-06-23 16:12:45Z jforest $ *)
+(* $Id: FSetAVL.v 9862 2007-05-25 16:57:06Z letouzey $ *)
 
 (** This module implements sets using AVL trees.
     It follows the implementation from Ocaml's standard library. *)
@@ -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 6fa6a85c..28a5705d 100644
--- a/theories/FSets/OrderedTypeEx.v
+++ b/theories/FSets/OrderedTypeEx.v
@@ -11,7 +11,7 @@
  * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
  *              91405 Orsay, France *)
 
-(* $Id: OrderedTypeEx.v 9066 2006-08-14 10:11:18Z letouzey $ *)
+(* $Id: OrderedTypeEx.v 9940 2007-07-05 12:32:47Z letouzey $ *)
 
 Require Import OrderedType.
 Require Import ZArith.
@@ -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.
@@ -138,14 +138,14 @@ Module Positive_as_OT <: UsualOrderedType.
   apply GT; unfold lt.
   replace Eq with (CompOpp Eq); auto.
   rewrite <- Pcompare_antisym; rewrite H; auto.
-  Qed.
+  Defined.
 
 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.