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.

22 files changed, 36 insertions, 38 deletions

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. *)
 
diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index 80a5d753..3d4e8661 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -44,7 +44,7 @@ Require Import Floats.
 Require Import Op.
 Require Import CminorSel.
 
-Open Local Scope cminorsel_scope.
+Local Open Scope cminorsel_scope.
 
 (** ** Constants **)
 
diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index e520b3cf..dd194498 100644
--- a/arm/SelectOpproof.v
+++ b/arm/SelectOpproof.v
@@ -25,7 +25,7 @@ Require Import Op.
 Require Import CminorSel.
 Require Import SelectOp.
 
-Open Local Scope cminorsel_scope.
+Local Open Scope cminorsel_scope.
 Local Transparent Archi.ptr64.
 
 (** * Useful lemmas and tactics *)
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index ace822fd..b635fd58 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -1082,7 +1082,7 @@ End CORRECTNESS_EXPR.
 
 (** ** Measure over CminorSel states *)
 
-Open Local Scope nat_scope.
+Local Open Scope nat_scope.
 
 Fixpoint size_stmt (s: stmt) : nat :=
   match s with
diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp
index 5cc66322..dc85fb25 100644
--- a/backend/SelectDiv.vp
+++ b/backend/SelectDiv.vp
@@ -17,7 +17,7 @@ Require Import Compopts.
 Require Import AST Integers Floats.
 Require Import Op CminorSel SelectOp SplitLong SelectLong.
 
-Open Local Scope cminorsel_scope.
+Local Open Scope cminorsel_scope.
 
 (** We try to turn divisions by a constant into a multiplication by
   a pseudo-inverse of the divisor.  The approach is described in
diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v
index 3180a55d..2ca30e52 100644
--- a/backend/SelectDivproof.v
+++ b/backend/SelectDivproof.v
@@ -17,7 +17,7 @@ Require Import AST Integers Floats Values Memory Globalenvs Events.
 Require Import Cminor Op CminorSel.
 Require Import SelectOp SelectOpproof SplitLong SplitLongproof SelectLong SelectLongproof SelectDiv.
 
-Open Local Scope cminorsel_scope.
+Local Open Scope cminorsel_scope.
 
 (** * Main approximation theorems *)
 
diff --git a/backend/SplitLongproof.v b/backend/SplitLongproof.v
index 8c8dea2f..3b1eaa6b 100644
--- a/backend/SplitLongproof.v
+++ b/backend/SplitLongproof.v
@@ -18,8 +18,8 @@ Require Import AST Errors Integers Floats.
 Require Import Values Memory Globalenvs Events Cminor Op CminorSel.
 Require Import SelectOp SelectOpproof SplitLong.
 
-Open Local Scope cminorsel_scope.
-Open Local Scope string_scope.
+Local Open Scope cminorsel_scope.
+Local Open Scope string_scope.
 
 (** * Axiomatization of the helper functions *)
 
diff --git a/backend/Stacking.v b/backend/Stacking.v
index 700025c2..f51848f2 100644
--- a/backend/Stacking.v
+++ b/backend/Stacking.v
@@ -169,7 +169,7 @@ Definition transl_code
 Definition transl_body (f: Linear.function) (fe: frame_env) :=
   save_callee_save fe (transl_code fe f.(Linear.fn_code)).
 
-Open Local Scope string_scope.
+Local Open Scope string_scope.
 
 Definition transf_function (f: Linear.function) : res Mach.function :=
   let fe := make_env (function_bounds f) in
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.
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index aeb31fe2..792a73f9 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -24,8 +24,8 @@ Require Import Coqlib Maps Errors Integers Floats.
 Require Import AST Linking.
 Require Import Ctypes Cop Clight Cminor Csharpminor.
 
-Open Local Scope string_scope.
-Open Local Scope error_monad_scope.
+Local Open Scope string_scope.
+Local Open Scope error_monad_scope.
 
 (** * Csharpminor constructors *)
 
diff --git a/common/Errors.v b/common/Errors.v
index 338d777d..293b7993 100644
--- a/common/Errors.v
+++ b/common/Errors.v
@@ -104,7 +104,7 @@ Notation "'assertion' A ; B" := (if A then B else assertion_failed)
 
 (** This is the familiar monadic map iterator. *)
 
-Open Local Scope error_monad_scope.
+Local Open Scope error_monad_scope.
 
 Fixpoint mmap (A B: Type) (f: A -> res B) (l: list A) {struct l} : res (list B) :=
   match l with
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' ->
diff --git a/driver/Compiler.v b/driver/Compiler.v
index dd752aca..5ced13e1 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -80,7 +80,7 @@ Parameter print_RTL: Z -> RTL.program -> unit.
 Parameter print_LTL: LTL.program -> unit.
 Parameter print_Mach: Mach.program -> unit.
 
-Open Local Scope string_scope.
+Local Open Scope string_scope.
 
 (** * Composing the translation passes *)
 
diff --git a/lib/Lattice.v b/lib/Lattice.v
index 4455e22f..6eebca99 100644
--- a/lib/Lattice.v
+++ b/lib/Lattice.v
@@ -56,7 +56,7 @@ End SEMILATTICE.
 
 Module Type SEMILATTICE_WITH_TOP.
 
-  Include Type SEMILATTICE.
+  Include SEMILATTICE.
   Parameter top: t.
   Axiom ge_top: forall x, ge top x.
 
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 799d208e..fc04b15d 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -22,8 +22,8 @@ Require Import Locations.
 Require Import Mach.
 Require Import Asm.
 
-Open Local Scope string_scope.
-Open Local Scope error_monad_scope.
+Local Open Scope string_scope.
+Local Open Scope error_monad_scope.
 
 (** The code generation functions take advantage of several
   characteristics of the [Mach] code generated by earlier passes of the
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index 79f05295..b5e3ed7e 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -44,7 +44,7 @@ Require Import Floats.
 Require Import Op.
 Require Import CminorSel.
 
-Open Local Scope cminorsel_scope.
+Local Open Scope cminorsel_scope.
 
 (** ** Constants **)
 
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index e31e847a..548fbce2 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -26,7 +26,7 @@ Require Import Op.
 Require Import CminorSel.
 Require Import SelectOp.
 
-Open Local Scope cminorsel_scope.
+Local Open Scope cminorsel_scope.
 Local Transparent Archi.ptr64.
 
 (** * Useful lemmas and tactics *)
diff --git a/x86/Asmgen.v b/x86/Asmgen.v
index bb26d507..a627881b 100644
--- a/x86/Asmgen.v
+++ b/x86/Asmgen.v
@@ -16,8 +16,8 @@ Require Import Coqlib Errors.
 Require Import AST Integers Floats Memdata.
 Require Import Op Locations Mach Asm.
 
-Open Local Scope string_scope.
-Open Local Scope error_monad_scope.
+Local Open Scope string_scope.
+Local Open Scope error_monad_scope.
 
 (** The code generation functions take advantage of several characteristics of the [Mach] code generated by earlier passes of the compiler:
 - Argument and result registers are of the correct type.
diff --git a/x86/Asmgenproof1.v b/x86/Asmgenproof1.v
index 401be7d7..6191ea39 100644
--- a/x86/Asmgenproof1.v
+++ b/x86/Asmgenproof1.v
@@ -17,7 +17,7 @@ Require Import AST Errors Integers Floats Values Memory Globalenvs.
 Require Import Op Locations Conventions Mach Asm.
 Require Import Asmgen Asmgenproof0.
 
-Open Local Scope error_monad_scope.
+Local Open Scope error_monad_scope.
 
 (** * Correspondence between Mach registers and x86 registers *)
 
diff --git a/x86/SelectLongproof.v b/x86/SelectLongproof.v
index f7d5df10..2262a70b 100644
--- a/x86/SelectLongproof.v
+++ b/x86/SelectLongproof.v
@@ -19,8 +19,8 @@ Require Import Cminor Op CminorSel.
 Require Import SelectOp SelectOpproof SplitLong SplitLongproof.
 Require Import SelectLong.
 
-Open Local Scope cminorsel_scope.
-Open Local Scope string_scope.
+Local Open Scope cminorsel_scope.
+Local Open Scope string_scope.
 
 (** * Correctness of the instruction selection functions for 64-bit operators *)
 
diff --git a/x86/SelectOp.vp b/x86/SelectOp.vp
index db546d99..f8010f0a 100644
--- a/x86/SelectOp.vp
+++ b/x86/SelectOp.vp
@@ -41,7 +41,7 @@ Require Import Compopts.
 Require Import AST Integers Floats.
 Require Import Op CminorSel.
 
-Open Local Scope cminorsel_scope.
+Local Open Scope cminorsel_scope.
 
 (** ** Constants **)
 
diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v
index ce15b6e1..cdb79c6f 100644
--- a/x86/SelectOpproof.v
+++ b/x86/SelectOpproof.v
@@ -24,7 +24,7 @@ Require Import Op.
 Require Import CminorSel.
 Require Import SelectOp.
 
-Open Local Scope cminorsel_scope.
+Local Open Scope cminorsel_scope.
 
 (** * Useful lemmas and tactics *)