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

16 files changed, 16 insertions, 16 deletions

diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
index dd514653b..67039072b 100644
--- a/theories/Arith/Between.v
+++ b/theories/Arith/Between.v
@@ -9,7 +9,7 @@
 Require Import Le.
 Require Import Lt.
 
-Open Local Scope nat_scope.
+Local Open Scope nat_scope.
 
 Implicit Types k l p q r : nat.
 
diff --git a/theories/Arith/Bool_nat.v b/theories/Arith/Bool_nat.v
index f384e1488..f9c25739b 100644
--- a/theories/Arith/Bool_nat.v
+++ b/theories/Arith/Bool_nat.v
@@ -10,7 +10,7 @@ Require Export Compare_dec.
 Require Export Peano_dec.
 Require Import Sumbool.
 
-Open Local Scope nat_scope.
+Local Open Scope nat_scope.
 
 Implicit Types m n x y : nat.
 
diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v
index d0075d741..dc4da448e 100644
--- a/theories/Arith/Compare.v
+++ b/theories/Arith/Compare.v
@@ -8,7 +8,7 @@
 
 (** Equality is decidable on [nat] *)
 
-Open Local Scope nat_scope.
+Local Open Scope nat_scope.
 
 Implicit Types m n p q : nat.
 
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index cc2d8efb5..1cb91f9a5 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -11,7 +11,7 @@ Require Import Lt.
 Require Import Gt.
 Require Import Decidable.
 
-Open Local Scope nat_scope.
+Local Open Scope nat_scope.
 
 Implicit Types m n x y : nat.
 
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index 94986278c..1dc69f612 100644
--- a/theories/Arith/EqNat.v
+++ b/theories/Arith/EqNat.v
@@ -8,7 +8,7 @@
 
 (** Equality on natural numbers *)
 
-Open Local Scope nat_scope.
+Local Open Scope nat_scope.
 
 Implicit Types m n x y : nat.
 
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index cd4dae98e..9a84a7f2e 100644
--- a/theories/Arith/Even.v
+++ b/theories/Arith/Even.v
@@ -10,7 +10,7 @@
     and we prove the decidability and the exclusion of those predicates.
     The main results about parity are proved in the module Div2. *)
 
-Open Local Scope nat_scope.
+Local Open Scope nat_scope.
 
 Implicit Types m n : nat.
 
diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v
index e20626029..82643cdcd 100644
--- a/theories/Arith/Factorial.v
+++ b/theories/Arith/Factorial.v
@@ -9,7 +9,7 @@
 Require Import Plus.
 Require Import Mult.
 Require Import Lt.
-Open Local Scope nat_scope.
+Local Open Scope nat_scope.
 
 (** Factorial *)
 
diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v
index 32f453e59..f9bf0f2fd 100644
--- a/theories/Arith/Gt.v
+++ b/theories/Arith/Gt.v
@@ -15,7 +15,7 @@ Definition gt (n m:nat) := m < n.
 Require Import Le.
 Require Import Lt.
 Require Import Plus.
-Open Local Scope nat_scope.
+Local Open Scope nat_scope.
 
 Implicit Types m n p : nat.
 
diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
index f0ebf162b..717705a1c 100644
--- a/theories/Arith/Le.v
+++ b/theories/Arith/Le.v
@@ -16,7 +16,7 @@ where "n <= m" := (le n m) : nat_scope.
 >>
  *)
 
-Open Local Scope nat_scope.
+Local Open Scope nat_scope.
 
 Implicit Types m n p : nat.
 
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index e07bba8d9..1f7e6e018 100644
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -14,7 +14,7 @@ Infix "<" := lt : nat_scope.
 *)
 
 Require Import Le.
-Open Local Scope nat_scope.
+Local Open Scope nat_scope.
 
 Implicit Types m n p : nat.
 
diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v
index bcfbe0efe..18e0e6af2 100644
--- a/theories/Arith/Min.v
+++ b/theories/Arith/Min.v
@@ -10,7 +10,7 @@
 
 Require Import NPeano.
 
-Open Local Scope nat_scope.
+Local Open Scope nat_scope.
 Implicit Types m n p : nat.
 
 Notation min := Peano.min (only parsing).
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index ed215f540..7ec37a65e 100644
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -21,7 +21,7 @@ where "n - m" := (minus n m) : nat_scope.
 Require Import Lt.
 Require Import Le.
 
-Open Local Scope nat_scope.
+Local Open Scope nat_scope.
 
 Implicit Types m n p : nat.
 
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index 479138a98..64b0d4dd3 100644
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -11,7 +11,7 @@ Require Export Minus.
 Require Export Lt.
 Require Export Le.
 
-Open Local Scope nat_scope.
+Local Open Scope nat_scope.
 
 Implicit Types m n p : nat.
 
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index 6eb667c11..e68ba9590 100644
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -9,7 +9,7 @@
 Require Import Decidable.
 Require Eqdep_dec.
 Require Import Le Lt.
-Open Local Scope nat_scope.
+Local Open Scope nat_scope.
 
 Implicit Types m n x y : nat.
 
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index 02975d8f1..c036d06e1 100644
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -20,7 +20,7 @@ where "n + m" := (plus n m) : nat_scope.
 Require Import Le.
 Require Import Lt.
 
-Open Local Scope nat_scope.
+Local Open Scope nat_scope.
 
 Implicit Types m n p q : nat.
 
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index b4468dd1b..e264ccb5d 100644
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -10,7 +10,7 @@
 
 Require Import Lt.
 
-Open Local Scope nat_scope.
+Local Open Scope nat_scope.
 
 Implicit Types m n p : nat.