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/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v
index 06a1806..9d7bcc8 100644
--- a/mathcomp/fingroup/fingroup.v
+++ b/mathcomp/fingroup/fingroup.v
@@ -1242,7 +1242,7 @@ Structure group_type : Type := Group {
 }.
 
 Definition group_of of phant gT : predArgType := group_type.
-Notation Local groupT := (group_of (Phant gT)).
+Local Notation groupT := (group_of (Phant gT)).
 Identity Coercion type_of_group : group_of >-> group_type.
 
 Canonical group_subType := Eval hnf in [subType for gval].
diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v
index 4ee2bc8..94304c4 100644
--- a/mathcomp/fingroup/gproduct.v
+++ b/mathcomp/fingroup/gproduct.v
@@ -1337,7 +1337,7 @@ Hypothesis nHK : K \subset 'N(H).
 Hypothesis actf : {in H & K, morph_act 'J 'J fH fK}.
 Hypothesis eqfHK : {in H :&: K, fH =1 fK}.
 
-Notation Local f := (pprodm nHK actf eqfHK).
+Local Notation f := (pprodm nHK actf eqfHK).
 
 Lemma pprodmE x a : x \in H -> a \in K -> f (x * a) = fH x * fK a.
 Proof.
diff --git a/mathcomp/fingroup/morphism.v b/mathcomp/fingroup/morphism.v
index 9f0a900..2a70706 100644
--- a/mathcomp/fingroup/morphism.v
+++ b/mathcomp/fingroup/morphism.v
@@ -1006,7 +1006,7 @@ Variables (G : {group gT}) (H : {group hT}).
 Variable f : {morphism G >-> hT}.
 Variable g : {morphism H >-> rT}.
 
-Notation Local gof := (mfun g \o mfun f).
+Local Notation gof := (mfun g \o mfun f).
 
 Lemma comp_morphM : {in f @*^-1 H &, {morph gof: x y / x * y}}.
 Proof.
diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v
index a306475..6d9abdc 100644
--- a/mathcomp/fingroup/perm.v
+++ b/mathcomp/fingroup/perm.v
@@ -87,8 +87,8 @@ Bind Scope group_scope with perm_of.
 Notation "''S_' n" := {perm 'I_n}
   (at level 8, n at level 2, format "''S_' n").
 
-Notation Local fun_of_perm_def := (fun T (u : perm_type T) => val u : T -> T).
-Notation Local perm_def := (fun T f injf => Perm (@perm_proof T f injf)).
+Local Notation fun_of_perm_def := (fun T (u : perm_type T) => val u : T -> T).
+Local Notation perm_def := (fun T f injf => Perm (@perm_proof T f injf)).
 
 Module Type PermDefSig.
 Parameter fun_of_perm : forall T, perm_type T -> T -> T.