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/ssreflect/seq.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/ssreflect/seq.v')

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.
 
-- 
cgit v1.2.3