From 3bd82b3cb10a721f2e2c8db6d0271c83a22095a3 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Mon, 13 Feb 2017 11:15:34 +0100
Subject: Use "Local" as prefix

Open Local becomes Local Open.  This silences Coq 8.6's warning.
Also: remove one useless Require-inside-a-module that caused another warning.
---
 arm/Asmgen.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'arm/Asmgen.v')

diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index bbfad3c9..e7a3b4fa 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -23,8 +23,8 @@ Require Import Mach.
 Require Import Asm.
 Require Import Compopts.
 
-Open Local Scope string_scope.
-Open Local Scope error_monad_scope.
+Local Open Scope string_scope.
+Local Open Scope error_monad_scope.
 
 (** Extracting integer or float registers. *)
 
-- 
cgit