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.
---
 common/Memory.v | 20 +++++++++-----------
 1 file changed, 9 insertions(+), 11 deletions(-)

(limited to 'common/Memory.v')

diff --git a/common/Memory.v b/common/Memory.v
index d0cbe8a0..764fdc26 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -96,7 +96,7 @@ Proof.
   intros; red; intros. subst b'. contradiction.
 Qed.
 
-Hint Local Resolve valid_not_valid_diff: mem.
+Local Hint Resolve valid_not_valid_diff: mem.
 
 (** Permissions *)
 
@@ -111,7 +111,7 @@ Proof.
   eapply perm_order_trans; eauto.
 Qed.
 
-Hint Local Resolve perm_implies: mem.
+Local Hint Resolve perm_implies: mem.
 
 Theorem perm_cur_max:
   forall m b ofs p, perm m b ofs Cur p -> perm m b ofs Max p.
@@ -138,7 +138,7 @@ Proof.
   intros. destruct k; auto. apply perm_cur_max. auto.
 Qed.
 
-Hint Local Resolve perm_cur perm_max: mem.
+Local Hint Resolve perm_cur perm_max: mem.
 
 Theorem perm_valid_block:
   forall m b ofs k p, perm m b ofs k p -> valid_block m b.
@@ -152,7 +152,7 @@ Proof.
   contradiction.
 Qed.
 
-Hint Local Resolve perm_valid_block: mem.
+Local Hint Resolve perm_valid_block: mem.
 
 Remark perm_order_dec:
   forall p1 p2, {perm_order p1 p2} + {~perm_order p1 p2}.
@@ -199,7 +199,7 @@ Proof.
   unfold range_perm; intros; eauto with mem.
 Qed.
 
-Hint Local Resolve range_perm_implies range_perm_cur range_perm_max: mem.
+Local Hint Resolve range_perm_implies range_perm_cur range_perm_max: mem.
 
 Lemma range_perm_dec:
   forall m b lo hi k p, {range_perm m b lo hi k p} + {~ range_perm m b lo hi k p}.
@@ -244,7 +244,7 @@ Proof.
   eapply valid_access_implies; eauto. constructor.
 Qed.
 
-Hint Local Resolve valid_access_implies: mem.
+Local Hint Resolve valid_access_implies: mem.
 
 Theorem valid_access_valid_block:
   forall m chunk b ofs,
@@ -257,7 +257,7 @@ Proof.
   eauto with mem.
 Qed.
 
-Hint Local Resolve valid_access_valid_block: mem.
+Local Hint Resolve valid_access_valid_block: mem.
 
 Lemma valid_access_perm:
   forall m chunk b ofs k p,
@@ -671,7 +671,7 @@ Proof.
   congruence.
 Qed.
 
-Hint Local Resolve load_valid_access valid_access_load: mem.
+Local Hint Resolve load_valid_access valid_access_load: mem.
 
 Theorem load_type:
   forall m chunk b ofs v,
@@ -957,7 +957,7 @@ Proof.
   contradiction.
 Defined.
 
-Hint Local Resolve valid_access_store: mem.
+Local Hint Resolve valid_access_store: mem.
 
 Section STORE.
 Variable chunk: memory_chunk.
@@ -3378,8 +3378,6 @@ Proof.
   apply perm_cur_max. apply (H1 (Ptrofs.unsigned ofs2)). omega.
 Qed.
 
-Require Intv.
-
 Theorem disjoint_or_equal_inject:
   forall f m m' b1 b1' delta1 b2 b2' delta2 ofs1 ofs2 sz,
   inject f m m' ->
-- 
cgit