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, 7 insertions, 7 deletions

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