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

(limited to 'mathcomp/algebra/vector.v')

diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v
index da6dc59..b7a9052 100644
--- a/mathcomp/algebra/vector.v
+++ b/mathcomp/algebra/vector.v
@@ -93,7 +93,7 @@ Require Import finfun tuple ssralg matrix mxalgebra zmodp.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
-Open Local Scope ring_scope.
+Local Open Scope ring_scope.
 
 Reserved Notation "{ 'vspace' T }" (at level 0, format "{ 'vspace'  T }").
 Reserved Notation "''Hom' ( T , rT )" (at level 8, format "''Hom' ( T ,  rT )").
-- 
cgit v1.2.3