Open Local Scope ---> Local Open Scope, same with Notation and alii

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

6 files changed, 6 insertions, 6 deletions

diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v
index cac3cd4e5..8d535d509 100644
--- a/theories/ZArith/ZArith_dec.v
+++ b/theories/ZArith/ZArith_dec.v
@@ -11,7 +11,7 @@ Require Import Sumbool.
 Require Import BinInt.
 Require Import Zorder.
 Require Import Zcompare.
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 (* begin hide *)
 (* Trivial, to deprecate? *)
diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v
index 3a86a821b..a38974339 100644
--- a/theories/ZArith/Zbool.v
+++ b/theories/ZArith/Zbool.v
@@ -13,7 +13,7 @@ Require Import Zcompare.
 Require Import ZArith_dec.
 Require Import Sumbool.
 
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 (** * Boolean operations from decidability of order *)
 (** The decidability of equality and order relations over
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index dde0745eb..7ae2a67ca 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -10,7 +10,7 @@ Require Import ZArithRing.
 Require Import ZArith_base.
 Require Export Omega.
 Require Import Wf_nat.
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 
 (**********************************************************************)
diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v
index bfd57d758..b871f9c98 100644
--- a/theories/ZArith/Zmisc.v
+++ b/theories/ZArith/Zmisc.v
@@ -11,7 +11,7 @@ Require Import BinInt.
 Require Import Zcompare.
 Require Import Zorder.
 Require Import Bool.
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 (**********************************************************************)
 (** Iterators *)
diff --git a/theories/ZArith/Zsqrt_compat.v b/theories/ZArith/Zsqrt_compat.v
index 54f6f2e9a..0a5ad4ace 100644
--- a/theories/ZArith/Zsqrt_compat.v
+++ b/theories/ZArith/Zsqrt_compat.v
@@ -9,7 +9,7 @@
 Require Import ZArithRing.
 Require Import Omega.
 Require Export ZArith_base.
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 (**  THIS FILE IS DEPRECATED
 
diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v
index efe5b6847..0a4418671 100644
--- a/theories/ZArith/Zwf.v
+++ b/theories/ZArith/Zwf.v
@@ -9,7 +9,7 @@
 Require Import ZArith_base.
 Require Export Wf_nat.
 Require Import Omega.
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 (** Well-founded relations on Z. *)