From 5e7d37af933a6548b2194adb5ceeaff30e6bb3cb Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 25 May 2007 16:46:27 +0000 Subject: 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 --- theories/FSets/FMapAVL.v | 6 +++--- theories/FSets/FMapPositive.v | 2 +- theories/FSets/FSetAVL.v | 4 ++-- theories/FSets/OrderedTypeEx.v | 6 +++--- 4 files changed, 9 insertions(+), 9 deletions(-) (limited to 'theories') 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. -- cgit v1.2.3