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/field/falgebra.v  | 2 +-
 mathcomp/field/separable.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp/field')

diff --git a/mathcomp/field/falgebra.v b/mathcomp/field/falgebra.v
index 58eccc2..23f5cba 100644
--- a/mathcomp/field/falgebra.v
+++ b/mathcomp/field/falgebra.v
@@ -79,7 +79,7 @@ Require Import div tuple finfun bigop ssralg finalg zmodp matrix vector poly.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
-Open Local Scope ring_scope.
+Local Open Scope ring_scope.
 
 Reserved Notation "{ 'aspace' T }" (at level 0, format "{ 'aspace'  T }").
 Reserved Notation "<< U & vs >>" (at level 0, format "<< U  &  vs >>").
diff --git a/mathcomp/field/separable.v b/mathcomp/field/separable.v
index e8b8944..6178c01 100644
--- a/mathcomp/field/separable.v
+++ b/mathcomp/field/separable.v
@@ -34,7 +34,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Open Local Scope ring_scope.
+Local Open Scope ring_scope.
 Import GRing.Theory.
 
 Section SeparablePoly.
-- 
cgit v1.2.3