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

(limited to 'cfrontend/Cminorgenproof.v')

diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index ea1bc89c..a6d58f17 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -20,7 +20,7 @@ Require Import AST Linking.
 Require Import Values Memory Events Globalenvs Smallstep.
 Require Import Csharpminor Switch Cminor Cminorgen.
 
-Open Local Scope error_monad_scope.
+Local Open Scope error_monad_scope.
 
 Definition match_prog (p: Csharpminor.program) (tp: Cminor.program) :=
   match_program (fun cu f tf => transl_fundef f = OK tf) eq p tp.
-- 
cgit