diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-02-13 11:15:34 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-02-13 11:15:34 +0100 |
commit | 3bd82b3cb10a721f2e2c8db6d0271c83a22095a3 (patch) | |
tree | 5bcb0ee57b1ab5f8083594f0596edcf1cd3990e8 | |
parent | c736e7d34560fef54ec4ab652be28bf2df4e907f (diff) | |
download | compcert-kvx-3bd82b3cb10a721f2e2c8db6d0271c83a22095a3.tar.gz compcert-kvx-3bd82b3cb10a721f2e2c8db6d0271c83a22095a3.zip |
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.
-rw-r--r-- | arm/Asmgen.v | 4 | ||||
-rw-r--r-- | arm/SelectOp.vp | 2 | ||||
-rw-r--r-- | arm/SelectOpproof.v | 2 | ||||
-rw-r--r-- | backend/RTLgenproof.v | 2 | ||||
-rw-r--r-- | backend/SelectDiv.vp | 2 | ||||
-rw-r--r-- | backend/SelectDivproof.v | 2 | ||||
-rw-r--r-- | backend/SplitLongproof.v | 4 | ||||
-rw-r--r-- | backend/Stacking.v | 2 | ||||
-rw-r--r-- | cfrontend/Cminorgenproof.v | 2 | ||||
-rw-r--r-- | cfrontend/Cshmgen.v | 4 | ||||
-rw-r--r-- | common/Errors.v | 2 | ||||
-rw-r--r-- | common/Memory.v | 20 | ||||
-rw-r--r-- | driver/Compiler.v | 2 | ||||
-rw-r--r-- | lib/Lattice.v | 2 | ||||
-rw-r--r-- | powerpc/Asmgen.v | 4 | ||||
-rw-r--r-- | powerpc/SelectOp.vp | 2 | ||||
-rw-r--r-- | powerpc/SelectOpproof.v | 2 | ||||
-rw-r--r-- | x86/Asmgen.v | 4 | ||||
-rw-r--r-- | x86/Asmgenproof1.v | 2 | ||||
-rw-r--r-- | x86/SelectLongproof.v | 4 | ||||
-rw-r--r-- | x86/SelectOp.vp | 2 | ||||
-rw-r--r-- | x86/SelectOpproof.v | 2 |
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 *) |