Fix obsolete vernacular syntax for locality.

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

9 files changed, 33 insertions, 33 deletions

diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v
index c5d2ef3..a517c8a 100644
--- a/mathcomp/ssreflect/bigop.v
+++ b/mathcomp/ssreflect/bigop.v
@@ -1094,14 +1094,14 @@ Import Monoid.Theory.
 Variable R : Type.
 
 Variable idx : R.
-Notation Local "1" := idx.
+Local Notation "1" := idx.
 
 Section Plain.
 
 Variable op : Monoid.law 1.
 
-Notation Local "*%M" := op (at level 0).
-Notation Local "x * y" := (op x y).
+Local Notation "*%M" := op (at level 0).
+Local Notation "x * y" := (op x y).
 
 Lemma eq_big_idx_seq idx' I r (P : pred I) F :
      right_id idx' *%M -> has P r ->
@@ -1226,8 +1226,8 @@ Section Abelian.
 
 Variable op : Monoid.com_law 1.
 
-Notation Local "'*%M'" := op (at level 0).
-Notation Local "x * y" := (op x y).
+Local Notation "'*%M'" := op (at level 0).
+Local Notation "x * y" := (op x y).
 
 Lemma eq_big_perm (I : eqType) r1 r2 (P : pred I) F :
     perm_eq r1 r2 ->
@@ -1517,14 +1517,14 @@ Import Monoid.Theory.
 
 Variable R : Type.
 Variables zero one : R.
-Notation Local "0" := zero.
-Notation Local "1" := one.
+Local Notation "0" := zero.
+Local Notation "1" := one.
 Variable times : Monoid.mul_law 0.
-Notation Local "*%M" := times (at level 0).
-Notation Local "x * y" := (times x y).
+Local Notation "*%M" := times (at level 0).
+Local Notation "x * y" := (times x y).
 Variable plus : Monoid.add_law 0 *%M.
-Notation Local "+%M" := plus (at level 0).
-Notation Local "x + y" := (plus x y).
+Local Notation "+%M" := plus (at level 0).
+Local Notation "x + y" := (plus x y).
 
 Lemma big_distrl I r a (P : pred I) F :
   \big[+%M/0]_(i <- r | P i) F i * a = \big[+%M/0]_(i <- r | P i) (F i * a).
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index e11fd9f..3e8230e 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -696,7 +696,7 @@ Section SubEqType.
 
 Variables (T : eqType) (P : pred T) (sT : subType P).
 
-Notation Local ev_ax := (fun T v => @Equality.axiom T (fun x y => v x == v y)).
+Local Notation ev_ax := (fun T v => @Equality.axiom T (fun x y => v x == v y)).
 Lemma val_eqP : ev_ax sT val. Proof. exact: inj_eqAxiom val_inj. Qed.
 
 Definition sub_eqMixin := EqMixin val_eqP.
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index feac3ab..a9899b7 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -151,9 +151,9 @@ Notation "A :!=: B" := (A != B :> {set _})
 Notation "A :=P: B" := (A =P B :> {set _})
   (at level 70, no associativity, only parsing) : set_scope.
 
-Notation Local finset_def := (fun T P => @FinSet T (finfun P)).
+Local Notation finset_def := (fun T P => @FinSet T (finfun P)).
 
-Notation Local pred_of_set_def := (fun T (A : set_type T) => val A : _ -> _).
+Local Notation pred_of_set_def := (fun T (A : set_type T) => val A : _ -> _).
 
 Module Type SetDefSig.
 Parameter finset : forall T : finType, pred T -> {set T}.
@@ -1021,9 +1021,9 @@ End CartesianProd.
 Implicit Arguments setXP [x1 x2 fT1 fT2 A1 A2].
 Prenex Implicits setXP.
 
-Notation Local imset_def :=
+Local Notation imset_def :=
   (fun (aT rT : finType) f mD => [set y in @image_mem aT rT f mD]).
-Notation Local imset2_def :=
+Local Notation imset2_def :=
   (fun (aT1 aT2 rT : finType) f (D1 : mem_pred aT1) (D2 : _ -> mem_pred aT2) =>
      [set y in @image_mem _ rT (prod_curry f)
                            (mem [pred u | D1 u.1 & D2 u.1 u.2])]).
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 215c69b..1171fcb 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -430,8 +430,8 @@ Notation "[ 'disjoint' A & B ]" := (disjoint (mem A) (mem B))
   (at level 0,
    format "'[hv' [ 'disjoint' '/  '  A '/'  &  B ] ']'") : bool_scope.
 
-Notation Local subset_type := (forall (T : finType) (A B : mem_pred T), bool).
-Notation Local subset_def := (fun T A B => pred0b (predD A B)).
+Local Notation subset_type := (forall (T : finType) (A B : mem_pred T), bool).
+Local Notation subset_def := (fun T A B => pred0b (predD A B)).
 Module Type SubsetDefSig.
 Parameter subset : subset_type. Axiom subsetEdef : subset = subset_def.
 End SubsetDefSig.
diff --git a/mathcomp/ssreflect/plugin/v8.5/ssrbool.v b/mathcomp/ssreflect/plugin/v8.5/ssrbool.v
index c5a881f..f81e16e 100644
--- a/mathcomp/ssreflect/plugin/v8.5/ssrbool.v
+++ b/mathcomp/ssreflect/plugin/v8.5/ssrbool.v
@@ -1506,17 +1506,17 @@ Proof. by move=> trR x y z Ryx Rzy; apply: trR Rzy Ryx. Qed.
 
 (* Property localization *)
 
-Notation Local "{ 'all1' P }" := (forall x, P x : Prop) (at level 0).
-Notation Local "{ 'all2' P }" := (forall x y, P x y : Prop) (at level 0).
-Notation Local "{ 'all3' P }" := (forall x y z, P x y z: Prop) (at level 0).
-Notation Local ph := (phantom _).
+Local Notation "{ 'all1' P }" := (forall x, P x : Prop) (at level 0).
+Local Notation "{ 'all2' P }" := (forall x y, P x y : Prop) (at level 0).
+Local Notation "{ 'all3' P }" := (forall x y z, P x y z: Prop) (at level 0).
+Local Notation ph := (phantom _).
 
 Section LocalProperties.
 
 Variables T1 T2 T3 : Type.
 
 Variables (d1 : mem_pred T1) (d2 : mem_pred T2) (d3 : mem_pred T3).
-Notation Local ph := (phantom Prop).
+Local Notation ph := (phantom Prop).
 
 Definition prop_for (x : T1) P & ph {all1 P} := P x.
 
diff --git a/mathcomp/ssreflect/plugin/v8.6/ssrbool.v b/mathcomp/ssreflect/plugin/v8.6/ssrbool.v
index c5a881f..f81e16e 100644
--- a/mathcomp/ssreflect/plugin/v8.6/ssrbool.v
+++ b/mathcomp/ssreflect/plugin/v8.6/ssrbool.v
@@ -1506,17 +1506,17 @@ Proof. by move=> trR x y z Ryx Rzy; apply: trR Rzy Ryx. Qed.
 
 (* Property localization *)
 
-Notation Local "{ 'all1' P }" := (forall x, P x : Prop) (at level 0).
-Notation Local "{ 'all2' P }" := (forall x y, P x y : Prop) (at level 0).
-Notation Local "{ 'all3' P }" := (forall x y z, P x y z: Prop) (at level 0).
-Notation Local ph := (phantom _).
+Local Notation "{ 'all1' P }" := (forall x, P x : Prop) (at level 0).
+Local Notation "{ 'all2' P }" := (forall x y, P x y : Prop) (at level 0).
+Local Notation "{ 'all3' P }" := (forall x y z, P x y z: Prop) (at level 0).
+Local Notation ph := (phantom _).
 
 Section LocalProperties.
 
 Variables T1 T2 T3 : Type.
 
 Variables (d1 : mem_pred T1) (d2 : mem_pred T2) (d3 : mem_pred T3).
-Notation Local ph := (phantom Prop).
+Local Notation ph := (phantom Prop).
 
 Definition prop_for (x : T1) P & ph {all1 P} := P x.
 
diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index 5c6acce..41243ea 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/mathcomp/ssreflect/prime.v
@@ -105,7 +105,7 @@ Definition pfactor p e := p ^ e.
 
 Definition cons_pfactor (p e : nat) pd := ifnz e ((p, e) :: pd) pd.
 
-Notation Local "p ^? e :: pd" := (cons_pfactor p e pd)
+Local Notation "p ^? e :: pd" := (cons_pfactor p e pd)
   (at level 30, e at level 30, pd at level 60) : nat_scope.
 
 Section prime_decomp.
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 32f507d..9ff9f61 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -856,7 +856,7 @@ Implicit Arguments revK [[T]].
 Section EqSeq.
 
 Variables (n0 : nat) (T : eqType) (x0 : T).
-Notation Local nth := (nth x0).
+Local Notation nth := (nth x0).
 Implicit Type s : seq T.
 Implicit Types x y z : T.
 
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index 4b9523f..8c21ae4 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -1395,10 +1395,10 @@ Definition exp m n := if n is n'.+1 then mul_exp m n' m else 1.
 
 Notation "n ^ m" := (exp n m) : nat_scope.
 
-Notation Local oddn := odd.
+Local Notation oddn := odd.
 Fixpoint odd n := if n is n'.+2 then odd n' else eqn n 1.
 
-Notation Local doublen := double.
+Local Notation doublen := double.
 Definition double n := if n is n'.+1 then n' + n.+1 else 0.
 Notation "n .*2" := (double n) : nat_scope.
 
@@ -1460,7 +1460,7 @@ Fixpoint nat_of_pos p0 :=
 
 End Trec.
 
-Coercion Local nat_of_pos : positive >-> nat.
+Local Coercion nat_of_pos : positive >-> nat.
 
 Coercion nat_of_bin b := if b is Npos p then p : nat else 0.