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

48 files changed, 54 insertions, 54 deletions

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 :