From e1b1743fb6aaed042d5e6762ea76c3242593ab1d Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 30 Oct 2017 14:16:48 +0100
Subject: Fix obsolete vernacular syntax for locality.

It was emitting a deprecation warning and will soon be removed from Coq.
---
 mathcomp/solvable/alt.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp/solvable/alt.v')

diff --git a/mathcomp/solvable/alt.v b/mathcomp/solvable/alt.v
index f43c89a..baf4792 100644
--- a/mathcomp/solvable/alt.v
+++ b/mathcomp/solvable/alt.v
@@ -36,7 +36,7 @@ Definition Sym of phant T : {set {perm T}} := setT.
 
 Canonical Sym_group phT := Eval hnf in [group of Sym phT].
 
-Notation Local "'Sym_T" := (Sym (Phant T)) (at level 0).
+Local Notation "'Sym_T" := (Sym (Phant T)) (at level 0).
 
 Canonical sign_morph := @Morphism _ _ 'Sym_T _ (in2W (@odd_permM _)).
 
@@ -44,7 +44,7 @@ Definition Alt of phant T := 'ker (@odd_perm T).
 
 Canonical Alt_group phT := Eval hnf in [group of Alt phT].
 
-Notation Local "'Alt_T" := (Alt (Phant T)) (at level 0).
+Local Notation "'Alt_T" := (Alt (Phant T)) (at level 0).
 
 Lemma Alt_even p : (p \in 'Alt_T) = ~~ p.
 Proof. by rewrite !inE /=; case: odd_perm. Qed.
-- 
cgit v1.2.3