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 /common/Memory.v | |
| 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.
Diffstat (limited to 'common/Memory.v')
| -rw-r--r-- | common/Memory.v | 20 |
1 files changed, 9 insertions, 11 deletions
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' -> |