Fix obsolete vernacular syntax for locality.

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

4 files changed, 5 insertions, 5 deletions

diff --git a/mathcomp/attic/amodule.v b/mathcomp/attic/amodule.v
index f4f80d0..d74288c 100644
--- a/mathcomp/attic/amodule.v
+++ b/mathcomp/attic/amodule.v
@@ -23,7 +23,7 @@ Require Import zmodp matrix vector falgebra galgebra.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
-Open Local Scope ring_scope.
+Local Open Scope ring_scope.
 
 Delimit Scope amodule_scope with aMS.
 
diff --git a/mathcomp/attic/fib.v b/mathcomp/attic/fib.v
index def96bb..fefa0d2 100644
--- a/mathcomp/attic/fib.v
+++ b/mathcomp/attic/fib.v
@@ -312,7 +312,7 @@ Qed.
 
 Section Matrix.
 
-Open Local Scope ring_scope.
+Local Open Scope ring_scope.
 Import GRing.Theory.
 
 Variable R: ringType.
diff --git a/mathcomp/attic/forms.v b/mathcomp/attic/forms.v
index 3ea6ab1..a1a987b 100644
--- a/mathcomp/attic/forms.v
+++ b/mathcomp/attic/forms.v
@@ -9,7 +9,7 @@ Require Import finfun tuple ssralg matrix zmodp vector.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
-Open Local Scope ring_scope.
+Local Open Scope ring_scope.
 
 Import GRing.Theory.
 
diff --git a/mathcomp/attic/galgebra.v b/mathcomp/attic/galgebra.v
index 5e12b38..4902a47 100644
--- a/mathcomp/attic/galgebra.v
+++ b/mathcomp/attic/galgebra.v
@@ -18,7 +18,7 @@ Unset Printing Implicit Defensive.
 Reserved Notation "g %:FG"
   (at level 2, left associativity, format "g %:FG").
 
-Open Local Scope ring_scope.
+Local Open Scope ring_scope.
 Import GRing.Theory.
 
 Section GroupAlgebraDef.
@@ -42,7 +42,7 @@ Lemma galgE : forall f, GAlg (finfun f) =1 f.
 Proof. by move=> f i; rewrite /fun_of_galg ffunE. Qed.
 
 Definition injG (g : gT) :=  GAlg ([ffun k => (k == g)%:R]).
-Notation Local "g %:FG" := (injG g).
+Local Notation "g %:FG" := (injG g).
 
 Implicit Types v: galg.