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

99 files changed, 115 insertions, 115 deletions

diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index 5ce5e0436..db4a5d3cd 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -1028,7 +1028,7 @@ You can use a what is called a hints' base.
 \begin{coq_example}
 Require Import ZArith.
 Require Ring.
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 Lemma toto1 : 1+1 = 2.
 ring.
 Qed.
@@ -1124,7 +1124,7 @@ Just use the {\ring} tactic.
 \begin{coq_example}
 Require Import ZArith.
 Require Ring.
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 Goal forall a b : Z, (a+b)*(a+b) = a*a + 2*a*b + b*b. 
 intros.
 ring.
@@ -1138,7 +1138,7 @@ Just use the {\field} tactic.
 \begin{coq_example}
 Require Import Reals.
 Require Ring.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 Goal forall a b : R, b*a<>0 -> (a/b) * (b/a) = 1. 
 intros.
 field.
@@ -1157,7 +1157,7 @@ Qed.
 \begin{coq_example}
 Require Import ZArith.
 Require Omega.
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 Goal forall a : Z, a>0 -> a+a > a. 
 intros.
 omega.
@@ -1310,7 +1310,7 @@ You need to use the {\try} and {\solve} tactics. For instance:
 \begin{coq_example}
 Require Import ZArith.
 Require Ring.
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 Goal forall a b c : Z, a+b=b+a.
 Proof with try solve [ring].
 intros...
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index ff85b629b..465ee925e 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -4091,7 +4091,7 @@ the tactic.
   No database name is given: the hint is registered in the {\tt core} 
     database. 
 
-\item\texttt{Hint Local} \textsl{hint\_definition} \texttt{:}
+\item\texttt{Local Hint} \textsl{hint\_definition} \texttt{:}
    \ident$_1$ \ldots\ \ident$_n$
 
   This is used to declare hints that must not be exported to the other
@@ -4099,7 +4099,7 @@ the tactic.
   section, the option {\tt Local} is useless since hints do not
   survive anyway to the closure of sections.
 
-\item\texttt{Hint Local} \textsl{hint\_definition} 
+\item\texttt{Local Hint} \textsl{hint\_definition}
 
   Idem for the {\tt core} database.
     
diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v
index bc08deaf9..cc6a7066a 100644
--- a/plugins/omega/PreOmega.v
+++ b/plugins/omega/PreOmega.v
@@ -8,7 +8,7 @@
 
 Require Import Arith Max Min BinInt BinNat Znat Nnat.
 
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 
 (** * zify: the Z-ification tactic *)
diff --git a/plugins/ring/LegacyArithRing.v b/plugins/ring/LegacyArithRing.v
index fd5bcd935..94dc48a73 100644
--- a/plugins/ring/LegacyArithRing.v
+++ b/plugins/ring/LegacyArithRing.v
@@ -13,7 +13,7 @@ Require Export LegacyRing.
 Require Export Arith.
 Require Import Eqdep_dec.
 
-Open Local Scope nat_scope.
+Local Open Scope nat_scope.
 
 Fixpoint nateq (n m:nat) {struct m} : bool :=
   match n, m with
diff --git a/plugins/setoid_ring/RealField.v b/plugins/setoid_ring/RealField.v
index 14c4270f9..1cbddc27d 100644
--- a/plugins/setoid_ring/RealField.v
+++ b/plugins/setoid_ring/RealField.v
@@ -5,7 +5,7 @@ Require Import Rdefinitions.
 Require Import Rpow_def.
 Require Import Raxioms.
 
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 Lemma RTheory : ring_theory 0 1 Rplus Rmult Rminus Ropp (eq (A:=R)).
 Proof.
diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v
index 28ab33af3..681c4716b 100644
--- a/test-suite/success/ProgramWf.v
+++ b/test-suite/success/ProgramWf.v
@@ -25,7 +25,7 @@ Print merge.
 Print Z.lt.
 Print Zwf.
 
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 Program Fixpoint Zwfrec (n m : Z) {measure (n + m) (Zwf 0)} : Z :=
   match n ?= m with
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index 79d12a061..12ddbda84 100644
--- a/test-suite/success/dependentind.v
+++ b/test-suite/success/dependentind.v
@@ -68,7 +68,7 @@ where " Γ ⊢ τ " := (term Γ τ) : type_scope.
 
 Hint Constructors term : lambda.
 
-Open Local Scope context_scope.
+Local Open Scope context_scope.
 
 Ltac eqns := subst ; reverse ; simplify_dep_elim ; simplify_IH_hyps.
 
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.
 
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 92a584256..79a719a1f 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -754,7 +754,7 @@ Notation "a &&& b" := (if a then b else false)
 Notation "a ||| b" := (if a then true else b)
  (at level 50, left associativity) : lazy_bool_scope.
 
-Open Local Scope lazy_bool_scope.
+Local Open Scope lazy_bool_scope.
 
 Lemma andb_lazy_alt : forall a b : bool, a && b = a &&& b.
 Proof.
diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v
index 0c2181638..2f904c81b 100644
--- a/theories/Bool/Bvector.v
+++ b/theories/Bool/Bvector.v
@@ -13,7 +13,7 @@ Require Vector.
 Export Vector.VectorNotations.
 Require Import Minus.
 
-Open Local Scope nat_scope.
+Local Open Scope nat_scope.
 
 (**
 We build bit vectors in the spirit of List.v.
diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v
index bac4c0d69..5689bf50d 100644
--- a/theories/Bool/Zerob.v
+++ b/theories/Bool/Zerob.v
@@ -9,7 +9,7 @@
 Require Import Arith.
 Require Import Bool.
 
-Open Local Scope nat_scope.
+Local Open Scope nat_scope.
 
 Definition zerob (n:nat) : bool :=
   match n with
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index 87f86e0d3..29718276a 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -49,7 +49,7 @@ Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
     | right H => @left _ _ H
   end.
 
-Open Local Scope program_scope.
+Local Open Scope program_scope.
 
 (** Invert the branches. *)
 
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 6d550dc93..6b2e62c92 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -26,7 +26,7 @@ Unset Strict Implicit.
 Generalizable Variables A R eqA B S eqB.
 Local Obligation Tactic := simpl_relation.
 
-Open Local Scope signature_scope.
+Local Open Scope signature_scope.
 
 Definition equiv `{Equivalence A R} : relation A := R.
 
@@ -37,7 +37,7 @@ Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scop
 
 Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : equiv_scope.
 
-Open Local Scope equiv_scope.
+Local Open Scope equiv_scope.
 
 (** Overloading for [PER]. *)
 
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 8e491b1b8..0df835ab8 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -73,7 +73,7 @@ End ProperNotations.
 
 Export ProperNotations.
 
-Open Local Scope signature_scope.
+Local Open Scope signature_scope.
 
 (** [solve_proper] try to solve the goal [Proper (?==> ... ==>?) f]
     by repeated introductions and setoid rewrites. It should work
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 3717e1cb4..4c2c2dd0c 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -286,7 +286,7 @@ Definition predicate_implication {l : Tlist} :=
 Infix "<∙>" := predicate_equivalence (at level 95, no associativity) : predicate_scope.
 Infix "-∙>" := predicate_implication (at level 70, right associativity) : predicate_scope.
 
-Open Local Scope predicate_scope.
+Local Open Scope predicate_scope.
 
 (** The pointwise liftings of conjunction and disjunctions.
    Note that these are [binary_operation]s, building new relations out of old ones. *)
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index a090d2007..693b724bc 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -50,7 +50,7 @@ Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
 
 Require Import Coq.Program.Program.
 
-Open Local Scope program_scope.
+Local Open Scope program_scope.
 
 (** Invert the branches. *)
 
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 31a4f5f25..5eab6370b 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -146,7 +146,7 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y)
 
 Require Import Coq.Program.Tactics.
 
-Open Local Scope signature_scope.
+Local Open Scope signature_scope.
 
 Ltac red_subst_eq_morphism concl :=
   match concl with
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index c761e2a7b..bed5ce742 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -32,9 +32,9 @@ Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope.
    preservation *)
 
 Module Raw (Import I:Int)(X: OrderedType).
-Open Local Scope pair_scope.
-Open Local Scope lazy_bool_scope.
-Open Local Scope Int_scope.
+Local Open Scope pair_scope.
+Local Open Scope lazy_bool_scope.
+Local Open Scope Int_scope.
 
 Definition key := X.t.
 Hint Transparent key.
diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v
index 774bcd9b3..e1c603514 100644
--- a/theories/FSets/FMapFullAVL.v
+++ b/theories/FSets/FMapFullAVL.v
@@ -34,8 +34,8 @@ Module AvlProofs (Import I:Int)(X: OrderedType).
 Module Import Raw := Raw I X.
 Module Import II:=MoreInt(I).
 Import Raw.Proofs.
-Open Local Scope pair_scope.
-Open Local Scope Int_scope.
+Local Open Scope pair_scope.
+Local Open Scope Int_scope.
 
 Ltac omega_max := i2z_refl; romega with Z.
 
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index 6d0315b82..d562245d8 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -11,7 +11,7 @@
 Require Import Bool ZArith OrderedType OrderedTypeEx FMapInterface.
 
 Set Implicit Arguments.
-Open Local Scope positive_scope.
+Local Open Scope positive_scope.
 
 Local Unset Elimination Schemes.
 Local Unset Case Analysis Schemes.
diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v
index d35ed1389..653f7a70f 100644
--- a/theories/Logic/ClassicalDescription.v
+++ b/theories/Logic/ClassicalDescription.v
@@ -20,7 +20,7 @@ Require Export Classical.   (* Axiomatize classical reasoning *)
 Require Export Description. (* Axiomatize constructive form of Church's iota *)
 Require Import ChoiceFacts.
 
-Notation Local inhabited A := A (only parsing).
+Local Notation inhabited A := A (only parsing).
 
 (** The idea for the following proof comes from [ChicliPottierSimpson02] *)
 
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index 7d5cec74d..2e1e99e8a 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -117,7 +117,7 @@ Qed.
 
 *)
 
-Notation Local inhabited A := A (only parsing).
+Local Notation inhabited A := A (only parsing).
 
 Lemma prop_ext_A_eq_A_imp_A :
   prop_extensionality -> forall A:Prop, inhabited A -> (A -> A) = A.
diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v
index 8dd51482c..6885f70a9 100644
--- a/theories/Logic/ConstructiveEpsilon.v
+++ b/theories/Logic/ConstructiveEpsilon.v
@@ -112,7 +112,7 @@ of our searching algorithm. *)
 
 Let R (x y : nat) : Prop := x = S y /\ ~ P y.
 
-Notation Local acc x := (Acc R x).
+Local Notation acc x := (Acc R x).
 
 Lemma P_implies_acc : forall x : nat, P x -> acc x.
 Proof.
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index d1327af3e..e8e8b94ce 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -265,7 +265,7 @@ End ProofIrrel_RelChoice_imp_EqEM.
 
 (** Proof sketch from Bell [Bell93] (with thanks to P. Castéran) *)
 
-Notation Local inhabited A := A (only parsing).
+Local Notation inhabited A := A (only parsing).
 
 Section ExtensionalEpsilon_imp_EM.
 
@@ -279,7 +279,7 @@ Hypothesis epsilon_extensionality :
   forall (A:Type) (i:inhabited A) (P Q:A->Prop),
   (forall a, P a <-> Q a) -> epsilon A i P = epsilon A i Q.
 
-Notation Local eps := (epsilon bool true) (only parsing).
+Local Notation eps := (epsilon bool true) (only parsing).
 
 Theorem extensional_epsilon_imp_EM : forall P:Prop, P \/ ~ P.
 Proof.
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index 7cef5c5ad..f4ca4d680 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -29,7 +29,7 @@ Hint Unfold compose.
 Notation " g ∘ f " := (compose g f)
   (at level 40, left associativity) : program_scope.
 
-Open Local Scope program_scope.
+Local Open Scope program_scope.
 
 (** The non-dependent function space between [A] and [B]. *)
 
diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index 4642021c4..24baf4598 100644
--- a/theories/Program/Subset.v
+++ b/theories/Program/Subset.v
@@ -10,7 +10,7 @@
 Require Import Coq.Program.Utils.
 Require Import Coq.Program.Equality.
 
-Open Local Scope program_scope.
+Local Open Scope program_scope.
 
 (** The following tactics implement a poor-man's solution for proof-irrelevance: it tries to
    factorize every proof of the same proposition in a goal so that equality of such proofs becomes trivial. *)
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index ee0a7451b..8ef1eb4e6 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -12,7 +12,7 @@ Require Import Coq.Init.Wf.
 Require Import Coq.Program.Utils.
 Require Import ProofIrrelevance.
 
-Open Local Scope program_scope.
+Local Open Scope program_scope.
 
 Section Well_founded.
   Variable A : Type.
diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v
index cfc1fb141..54a6c3827 100644
--- a/theories/QArith/Qround.v
+++ b/theories/QArith/Qround.v
@@ -18,7 +18,7 @@ Hint Resolve Qopp_lt_compat : qarith.
 
 (************)
 
-Coercion Local inject_Z : Z >-> Q.
+Local Coercion inject_Z : Z >-> Q.
 
 Definition Qfloor (x:Q) := let (n,d) := x in Z.div n (Zpos d).
 Definition Qceiling (x:Q) := (-(Qfloor (-x)))%Z.
diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v
index 18612a687..5e91accfe 100644
--- a/theories/Reals/Alembert.v
+++ b/theories/Reals/Alembert.v
@@ -13,7 +13,7 @@ Require Import SeqProp.
 Require Import PartSum.
 Require Import Max.
 
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 (***************************************************)
 (* Various versions of the criterion of D'Alembert *)
diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v
index 87f1aaf72..227081cab 100644
--- a/theories/Reals/AltSeries.v
+++ b/theories/Reals/AltSeries.v
@@ -12,7 +12,7 @@ Require Import Rseries.
 Require Import SeqProp.
 Require Import PartSum.
 Require Import Max.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 (**********)
 (** * Formalization of alternated series *)
diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v
index 620561dcd..359b2855c 100644
--- a/theories/Reals/ArithProp.v
+++ b/theories/Reals/ArithProp.v
@@ -12,8 +12,8 @@ Require Import Even.
 Require Import Div2.
 Require Import ArithRing.
 
-Open Local Scope Z_scope.
-Open Local Scope R_scope.
+Local Open Scope Z_scope.
+Local Open Scope R_scope.
 
 Lemma minus_neq_O : forall n i:nat, (i < n)%nat -> (n - i)%nat <> 0%nat.
 Proof.
diff --git a/theories/Reals/Binomial.v b/theories/Reals/Binomial.v
index 412f64428..a7bb4d9a6 100644
--- a/theories/Reals/Binomial.v
+++ b/theories/Reals/Binomial.v
@@ -9,7 +9,7 @@
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import PartSum.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 Definition C (n p:nat) : R :=
   INR (fact n) / (INR (fact p) * INR (fact (n - p))).
diff --git a/theories/Reals/Cauchy_prod.v b/theories/Reals/Cauchy_prod.v
index a9d5cde38..3019be9e8 100644
--- a/theories/Reals/Cauchy_prod.v
+++ b/theories/Reals/Cauchy_prod.v
@@ -10,7 +10,7 @@ Require Import Rbase.
 Require Import Rfunctions.
 Require Import Rseries.
 Require Import PartSum.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
   (**********)
 Lemma sum_N_predN :
diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v
index ec1eeddf3..e966357ce 100644
--- a/theories/Reals/Cos_plus.v
+++ b/theories/Reals/Cos_plus.v
@@ -12,8 +12,8 @@ Require Import SeqSeries.
 Require Import Rtrigo_def.
 Require Import Cos_rel.
 Require Import Max.
-Open Local Scope nat_scope.
-Open Local Scope R_scope.
+Local Open Scope nat_scope.
+Local Open Scope R_scope.
 
 Definition Majxy (x y:R) (n:nat) : R :=
   Rmax 1 (Rmax (Rabs x) (Rabs y)) ^ (4 * S n) / INR (fact n).
diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v
index 73f3c0c64..204e2009d 100644
--- a/theories/Reals/Cos_rel.v
+++ b/theories/Reals/Cos_rel.v
@@ -10,7 +10,7 @@ Require Import Rbase.
 Require Import Rfunctions.
 Require Import SeqSeries.
 Require Import Rtrigo_def.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 Definition A1 (x:R) (N:nat) : R :=
   sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k)) * x ^ (2 * k)) N.
diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v
index 144de09e5..c21421b94 100644
--- a/theories/Reals/DiscrR.v
+++ b/theories/Reals/DiscrR.v
@@ -8,7 +8,7 @@
 
 Require Import RIneq.
 Require Import Omega.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 Lemma Rlt_R0_R2 : 0 < 2.
 change 2 with (INR 2); apply lt_INR_0; apply lt_O_Sn.
diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v
index 9a38888da..4b1b09406 100644
--- a/theories/Reals/Exp_prop.v
+++ b/theories/Reals/Exp_prop.v
@@ -15,8 +15,8 @@ Require Import PSeries_reg.
 Require Import Div2.
 Require Import Even.
 Require Import Max.
-Open Local Scope nat_scope.
-Open Local Scope R_scope.
+Local Open Scope nat_scope.
+Local Open Scope R_scope.
 
 Definition E1 (x:R) (N:nat) : R :=
   sum_f_R0 (fun k:nat => / INR (fact k) * x ^ k) N.
diff --git a/theories/Reals/MVT.v b/theories/Reals/MVT.v
index 29ebd46d8..b872e3fe3 100644
--- a/theories/Reals/MVT.v
+++ b/theories/Reals/MVT.v
@@ -10,7 +10,7 @@ Require Import Rbase.
 Require Import Rfunctions.
 Require Import Ranalysis1.
 Require Import Rtopology.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 (* The Mean Value Theorem *)
 Theorem MVT :
diff --git a/theories/Reals/Machin.v b/theories/Reals/Machin.v
index 503e79a40..6b91719db 100644
--- a/theories/Reals/Machin.v
+++ b/theories/Reals/Machin.v
@@ -9,7 +9,7 @@ Require Import SeqProp.
 Require Import PartSum.
 Require Import Ratan.
 
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 (* Proving a few formulas in the style of John Machin to compute Pi *)
 
diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v
index 8478a83e2..35192d0c4 100644
--- a/theories/Reals/NewtonInt.v
+++ b/theories/Reals/NewtonInt.v
@@ -11,7 +11,7 @@ Require Import Rfunctions.
 Require Import SeqSeries.
 Require Import Rtrigo1.
 Require Import Ranalysis.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 (*******************************************)
 (*            Newton's Integral            *)
diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v
index aa588e382..38de00030 100644
--- a/theories/Reals/PSeries_reg.v
+++ b/theories/Reals/PSeries_reg.v
@@ -12,7 +12,7 @@ Require Import SeqSeries.
 Require Import Ranalysis1.
 Require Import Max.
 Require Import Even.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 Definition Boule (x:R) (r:posreal) (y:R) : Prop := Rabs (y - x) < r.
 
diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v
index 3f90f15a0..3d9314b7d 100644
--- a/theories/Reals/PartSum.v
+++ b/theories/Reals/PartSum.v
@@ -11,7 +11,7 @@ Require Import Rfunctions.
 Require Import Rseries.
 Require Import Rcomplete.
 Require Import Max.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 Lemma tech1 :
   forall (An:nat -> R) (N:nat),
diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v
index dbd2e52ff..246d6dea9 100644
--- a/theories/Reals/RList.v
+++ b/theories/Reals/RList.v
@@ -8,7 +8,7 @@
 
 Require Import Rbase.
 Require Import Rfunctions.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 Inductive Rlist : Type :=
 | nil : Rlist
diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v
index c089b648d..9b64ea5f0 100644
--- a/theories/Reals/R_Ifp.v
+++ b/theories/Reals/R_Ifp.v
@@ -13,7 +13,7 @@
 
 Require Import Rbase.
 Require Import Omega.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 (*********************************************************)
 (** *    Fractional part                                 *)
diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v
index f23b9f178..868b8617f 100644
--- a/theories/Reals/R_sqr.v
+++ b/theories/Reals/R_sqr.v
@@ -8,7 +8,7 @@
 
 Require Import Rbase.
 Require Import Rbasic_fun.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 (****************************************************)
 (** Rsqr : some results                             *)
diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v
index 2c5ede239..47b9e6cf9 100644
--- a/theories/Reals/R_sqrt.v
+++ b/theories/Reals/R_sqrt.v
@@ -9,7 +9,7 @@
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Rsqrt_def.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 (** * Continuous extension of Rsqrt on R *)
 Definition sqrt (x:R) : R :=
diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v
index 3075bee8f..804bfe114 100644
--- a/theories/Reals/Ranalysis1.v
+++ b/theories/Reals/Ranalysis1.v
@@ -10,7 +10,7 @@ Require Import Rbase.
 Require Import Rfunctions.
 Require Export Rlimit.
 Require Export Rderiv.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 Implicit Type f : R -> R.
 
 (****************************************************)
@@ -43,7 +43,7 @@ Notation "- x" := (opp_fct x) : Rfun_scope.
 Infix "*" := mult_fct : Rfun_scope.
 Infix "-" := minus_fct : Rfun_scope.
 Infix "/" := div_fct : Rfun_scope.
-Notation Local "f1 'o' f2" := (comp f1 f2)
+Local Notation "f1 'o' f2" := (comp f1 f2)
   (at level 20, right associativity) : Rfun_scope.
 Notation "/ x" := (inv_fct x) : Rfun_scope.
 
diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v
index 732a61017..218f2a38f 100644
--- a/theories/Reals/Ranalysis2.v
+++ b/theories/Reals/Ranalysis2.v
@@ -9,7 +9,7 @@
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Ranalysis1.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 (**********)
 Lemma formule :
diff --git a/theories/Reals/Ranalysis3.v b/theories/Reals/Ranalysis3.v
index afd4a4ee8..aa9e6bb35 100644
--- a/theories/Reals/Ranalysis3.v
+++ b/theories/Reals/Ranalysis3.v
@@ -10,7 +10,7 @@ Require Import Rbase.
 Require Import Rfunctions.
 Require Import Ranalysis1.
 Require Import Ranalysis2.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 (** Division *)
 Theorem derivable_pt_lim_div :
diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v
index 9b6e550aa..83bc28318 100644
--- a/theories/Reals/Ranalysis4.v
+++ b/theories/Reals/Ranalysis4.v
@@ -13,7 +13,7 @@ Require Import Rtrigo1.
 Require Import Ranalysis1.
 Require Import Ranalysis3.
 Require Import Exp_prop.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 (**********)
 Lemma derivable_pt_inv :
diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v
index f6abd2b01..c8a2e1a83 100644
--- a/theories/Reals/Ranalysis5.v
+++ b/theories/Reals/Ranalysis5.v
@@ -6,7 +6,7 @@ Require Import Fourier.
 Require Import RiemannInt.
 Require Import SeqProp.
 Require Import Max.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 (** * Preliminaries lemmas *)
 
diff --git a/theories/Reals/Ranalysis_reg.v b/theories/Reals/Ranalysis_reg.v
index 2026dd82e..2d4a3f15c 100644
--- a/theories/Reals/Ranalysis_reg.v
+++ b/theories/Reals/Ranalysis_reg.v
@@ -26,7 +26,7 @@ Require Export RList.
 Require Export Sqrt_reg.
 Require Export Ranalysis4.
 Require Export Rpower.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 Axiom AppVar : R.
 
diff --git a/theories/Reals/Ratan.v b/theories/Reals/Ratan.v
index 01b429a08..597f95924 100644
--- a/theories/Reals/Ratan.v
+++ b/theories/Reals/Ratan.v
@@ -11,7 +11,7 @@ Require Import Ranalysis5.
 Require Import SeqSeries.
 Require Import PartSum.
 
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 (** Tools *)
 
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index 259e1ac04..6a5b778f6 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -12,7 +12,7 @@
 
 Require Export ZArith_base.
 Require Export Rdefinitions.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 (*********************************************************)
 (** *            Field axioms                            *)
diff --git a/theories/Reals/Rcomplete.v b/theories/Reals/Rcomplete.v
index 77cb560cc..2841ac8e3 100644
--- a/theories/Reals/Rcomplete.v
+++ b/theories/Reals/Rcomplete.v
@@ -11,7 +11,7 @@ Require Import Rfunctions.
 Require Import Rseries.
 Require Import SeqProp.
 Require Import Max.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 (****************************************************)
 (*              R is complete :                     *)
diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v
index 83c6b82de..6f9f92176 100644
--- a/theories/Reals/Rdefinitions.v
+++ b/theories/Reals/Rdefinitions.v
@@ -21,7 +21,7 @@ Delimit Scope R_scope with R.
 (* Automatically open scope R_scope for arguments of type R *)
 Bind Scope R_scope with R.
 
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 Parameter R0 : R.
 Parameter R1 : R.
diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v
index 8f9b99c28..0a6d728f5 100644
--- a/theories/Reals/Rderiv.v
+++ b/theories/Reals/Rderiv.v
@@ -16,7 +16,7 @@ Require Import Rfunctions.
 Require Import Rlimit.
 Require Import Fourier.
 Require Import Omega.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 (*********)
 Definition D_x (D:R -> Prop) (y x:R) : Prop := D x /\ y <> x.
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 4c4903cb2..940250273 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -535,7 +535,7 @@ Definition powerRZ (x:R) (n:Z) :=
     | Zneg p => / x ^ Pos.to_nat p
   end.
 
-Infix Local "^Z" := powerRZ (at level 30, right associativity) : R_scope.
+Local Infix "^Z" := powerRZ (at level 30, right associativity) : R_scope.
 
 Lemma Zpower_NR0 :
   forall (x:Z) (n:nat), (0 <= x)%Z -> (0 <= Zpower_nat x n)%Z.
diff --git a/theories/Reals/Rgeom.v b/theories/Reals/Rgeom.v
index 5715f07f4..c00917b6b 100644
--- a/theories/Reals/Rgeom.v
+++ b/theories/Reals/Rgeom.v
@@ -11,7 +11,7 @@ Require Import Rfunctions.
 Require Import SeqSeries.
 Require Import Rtrigo1.
 Require Import R_sqrt.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 (** * Distance *)
 
diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v
index 5b9c4bdd5..9e4a5e4b1 100644
--- a/theories/Reals/RiemannInt.v
+++ b/theories/Reals/RiemannInt.v
@@ -15,7 +15,7 @@ Require Import RiemannInt_SF.
 Require Import Classical_Prop.
 Require Import Classical_Pred_Type.
 Require Import Max.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 Set Implicit Arguments.
 
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v
index 18c24c184..abcb8d6ff 100644
--- a/theories/Reals/RiemannInt_SF.v
+++ b/theories/Reals/RiemannInt_SF.v
@@ -10,7 +10,7 @@ Require Import Rbase.
 Require Import Rfunctions.
 Require Import Ranalysis_reg.
 Require Import Classical_Prop.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 Set Implicit Arguments.
 
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index 80b900af7..d2fee1fde 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -14,7 +14,7 @@
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Fourier.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 (*******************************)
 (** *   Calculus               *)
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v
index b5bd2b734..019a2d96e 100644
--- a/theories/Reals/Rpower.v
+++ b/theories/Reals/Rpower.v
@@ -22,7 +22,7 @@ Require Import Rsqrt_def.
 Require Import R_sqrt.
 Require Import MVT.
 Require Import Ranalysis4.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 Lemma P_Rmin : forall (P:R -> Prop) (x y:R), P x -> P y -> P (Rmin x y).
 Proof.
@@ -394,7 +394,7 @@ Qed.
 
 Definition Rpower (x y:R) := exp (y * ln x).
 
-Infix Local "^R" := Rpower (at level 30, right associativity) : R_scope.
+Local Infix "^R" := Rpower (at level 30, right associativity) : R_scope.
 
 (******************************************************************)
 (** *                     Properties of  Rpower                   *)
diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v
index 12258d6b5..6bcf4bd4c 100644
--- a/theories/Reals/Rprod.v
+++ b/theories/Reals/Rprod.v
@@ -12,7 +12,7 @@ Require Import Rfunctions.
 Require Import Rseries.
 Require Import PartSum.
 Require Import Binomial.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 (** TT Ak; 0<=k<=N *)
 Fixpoint prod_f_R0 (f:nat -> R) (N:nat) : R :=
diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v
index 9d1ba7381..e67f118f6 100644
--- a/theories/Reals/Rseries.v
+++ b/theories/Reals/Rseries.v
@@ -9,7 +9,7 @@
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Compare.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 Implicit Type r : R.
 
diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v
index 0027c2749..d26dcde21 100644
--- a/theories/Reals/Rsigma.v
+++ b/theories/Reals/Rsigma.v
@@ -10,7 +10,7 @@ Require Import Rbase.
 Require Import Rfunctions.
 Require Import Rseries.
 Require Import PartSum.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 Set Implicit Arguments.
 
diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v
index 223649ef5..ecde4f8bb 100644
--- a/theories/Reals/Rsqrt_def.v
+++ b/theories/Reals/Rsqrt_def.v
@@ -11,7 +11,7 @@ Require Import Rbase.
 Require Import Rfunctions.
 Require Import SeqSeries.
 Require Import Ranalysis1.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 Fixpoint Dichotomy_lb (x y:R) (P:R -> bool) (N:nat) {struct N} : R :=
   match N with
diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v
index 814e336c2..77a4d5fbb 100644
--- a/theories/Reals/Rtopology.v
+++ b/theories/Reals/Rtopology.v
@@ -12,7 +12,7 @@ Require Import Ranalysis1.
 Require Import RList.
 Require Import Classical_Prop.
 Require Import Classical_Pred_Type.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 (** * General definitions and propositions *)
 
diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v
index 4a405660c..3bb07fe0c 100644
--- a/theories/Reals/Rtrigo_alt.v
+++ b/theories/Reals/Rtrigo_alt.v
@@ -10,7 +10,7 @@ Require Import Rbase.
 Require Import Rfunctions.
 Require Import SeqSeries.
 Require Import Rtrigo_def.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 (***************************************************************)
 (** Using series definitions of cos and sin                    *)
diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v
index 90ba205f6..e77ea6e2d 100644
--- a/theories/Reals/Rtrigo_calc.v
+++ b/theories/Reals/Rtrigo_calc.v
@@ -11,7 +11,7 @@ Require Import Rfunctions.
 Require Import SeqSeries.
 Require Import Rtrigo1.
 Require Import R_sqrt.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 Lemma tan_PI : tan PI = 0.
 Proof.
diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v
index 9b6edab68..2486e140f 100644
--- a/theories/Reals/Rtrigo_def.v
+++ b/theories/Reals/Rtrigo_def.v
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 Require Import Rbase Rfunctions SeqSeries Rtrigo_fun Max.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 (********************************)
 (** * Definition of exponential *)
diff --git a/theories/Reals/Rtrigo_fun.v b/theories/Reals/Rtrigo_fun.v
index 04deb0904..a946bc462 100644
--- a/theories/Reals/Rtrigo_fun.v
+++ b/theories/Reals/Rtrigo_fun.v
@@ -9,7 +9,7 @@
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import SeqSeries.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 (*****************************************************************)
 (**           To define transcendental functions                 *)
diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v
index 0a05e6df4..a369d5ae2 100644
--- a/theories/Reals/Rtrigo_reg.v
+++ b/theories/Reals/Rtrigo_reg.v
@@ -12,8 +12,8 @@ Require Import SeqSeries.
 Require Import Rtrigo1.
 Require Import Ranalysis1.
 Require Import PSeries_reg.
-Open Local Scope nat_scope.
-Open Local Scope R_scope.
+Local Open Scope nat_scope.
+Local Open Scope R_scope.
 
 
 (**********)
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v
index 7b6eadc2f..fb1b81ac3 100644
--- a/theories/Reals/SeqProp.v
+++ b/theories/Reals/SeqProp.v
@@ -10,7 +10,7 @@ Require Import Rbase.
 Require Import Rfunctions.
 Require Import Rseries.
 Require Import Max.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 (*****************************************************************)
 (**           Convergence properties of sequences                *)
diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v
index 0d876be5d..3085d0200 100644
--- a/theories/Reals/SeqSeries.v
+++ b/theories/Reals/SeqSeries.v
@@ -19,7 +19,7 @@ Require Export Rsigma.
 Require Export Rprod.
 Require Export Cauchy_prod.
 Require Export Alembert.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 (**********)
 Lemma sum_maj1 :
diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v
index 4e704a274..c429567fe 100644
--- a/theories/Reals/Sqrt_reg.v
+++ b/theories/Reals/Sqrt_reg.v
@@ -10,7 +10,7 @@ Require Import Rbase.
 Require Import Rfunctions.
 Require Import Ranalysis1.
 Require Import R_sqrt.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 (**********)
 Lemma sqrt_var_maj :
diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v
index 4f6fe3f86..c9e71e24a 100644
--- a/theories/Strings/Ascii.v
+++ b/theories/Strings/Ascii.v
@@ -137,7 +137,7 @@ Qed.
   which is typically not the case in coqide).
 *)
 
-Open Local Scope char_scope.
+Local Open Scope char_scope.
 
 Example Space := " ".
 Example DoubleQuote := """".
diff --git a/theories/Strings/String.v b/theories/Strings/String.v
index 958ecd4ff..289ffab31 100644
--- a/theories/Strings/String.v
+++ b/theories/Strings/String.v
@@ -24,7 +24,7 @@ Inductive string : Set :=
 
 Delimit Scope string_scope with string.
 Bind Scope string_scope with string.
-Open Local Scope string_scope.
+Local Open Scope string_scope.
 
 (** Equality is decidable *)
 
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. *)