Fix obsolete vernacular syntax for locality.

It was emitting a deprecation warning and will soon be removed from Coq.

6 files changed, 9 insertions, 9 deletions

diff --git a/mathcomp/algebra/fraction.v b/mathcomp/algebra/fraction.v
index 8cf811a..98eb9f1 100644
--- a/mathcomp/algebra/fraction.v
+++ b/mathcomp/algebra/fraction.v
@@ -16,8 +16,8 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 Import GRing.Theory.
-Open Local Scope ring_scope.
-Open Local Scope quotient_scope.
+Local Open Scope ring_scope.
+Local Open Scope quotient_scope.
 
 Reserved Notation "{ 'ratio' T }" (at level 0, format "{ 'ratio'  T }").
 Reserved Notation "{ 'fraction' T }" (at level 0, format "{ 'fraction'  T }").
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index 2aa117d..5f47691 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -147,7 +147,7 @@ Unset Printing Implicit Defensive.
 
 Import GroupScope.
 Import GRing.Theory.
-Open Local Scope ring_scope.
+Local Open Scope ring_scope.
 
 Reserved Notation "''M_' n"     (at level 8, n at level 2, format "''M_' n").
 Reserved Notation "''rV_' n"    (at level 8, n at level 2, format "''rV_' n").
@@ -193,7 +193,7 @@ Reserved Notation "\tr A"   (at level 10, A at level 8, format "\tr  A").
 Reserved Notation "\det A"  (at level 10, A at level 8, format "\det  A").
 Reserved Notation "\adj A"  (at level 10, A at level 8, format "\adj  A").
 
-Notation Local simp := (Monoid.Theory.simpm, oppr0).
+Local Notation simp := (Monoid.Theory.simpm, oppr0).
 
 (*****************************************************************************)
 (****************************Type Definition**********************************)
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v
index 3b3ca5d..da61dfb 100644
--- a/mathcomp/algebra/mxalgebra.v
+++ b/mathcomp/algebra/mxalgebra.v
@@ -135,7 +135,7 @@ Unset Printing Implicit Defensive.
 
 Import GroupScope.
 Import GRing.Theory.
-Open Local Scope ring_scope.
+Local Open Scope ring_scope.
 
 Reserved Notation "\rank A" (at level 10, A at level 8, format "\rank  A").
 Reserved Notation "A ^C"    (at level 8, format "A ^C").
@@ -160,7 +160,7 @@ Notation "''A' [ F ]_ n" := 'A[F]_(n)
 
 Delimit Scope matrix_set_scope with MS.
 
-Notation Local simp := (Monoid.Theory.simpm, oppr0).
+Local Notation simp := (Monoid.Theory.simpm, oppr0).
 
 (*****************************************************************************)
 (******************** Rank and row-space theory ******************************)
diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v
index 1301a94..eeece16 100644
--- a/mathcomp/algebra/mxpoly.v
+++ b/mathcomp/algebra/mxpoly.v
@@ -64,7 +64,7 @@ Unset Printing Implicit Defensive.
 Import GRing.Theory.
 Import Monoid.Theory.
 
-Open Local Scope ring_scope.
+Local Open Scope ring_scope.
 
 Import Pdiv.Idomain.
 (* Row vector <-> bounded degree polynomial bijection *)
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index 22caa4a..56493dd 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -101,7 +101,7 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 Import GRing.Theory.
-Open Local Scope ring_scope.
+Local Open Scope ring_scope.
 
 Reserved Notation "{ 'poly' T }" (at level 0, format "{ 'poly'  T }").
 Reserved Notation "c %:P" (at level 2, format "c %:P").
diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v
index da6dc59..b7a9052 100644
--- a/mathcomp/algebra/vector.v
+++ b/mathcomp/algebra/vector.v
@@ -93,7 +93,7 @@ Require Import finfun tuple ssralg matrix mxalgebra zmodp.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
-Open Local Scope ring_scope.
+Local Open Scope ring_scope.
 
 Reserved Notation "{ 'vspace' T }" (at level 0, format "{ 'vspace'  T }").
 Reserved Notation "''Hom' ( T , rT )" (at level 8, format "''Hom' ( T ,  rT )").