1 files changed, 17 insertions, 0 deletions
diff --git a/common/Memory.v b/common/Memory.v
index f21d99af..cd8a2001 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -1307,6 +1307,23 @@ Proof.
   }
 Qed.
     
+Section STOREV.
+Variable chunk: memory_chunk.
+Variable m1: mem.
+Variables addr v: val.
+Variable m2: mem.
+Hypothesis STORE: storev chunk m1 addr v = Some m2.
+
+
+Theorem loadv_storev_same:
+  loadv chunk m2 addr = Some (Val.load_result chunk v).
+Proof.
+  destruct addr; simpl in *; try discriminate.
+  eapply load_store_same.
+  eassumption.
+Qed.
+End STOREV.
+
 Lemma load_store_overlap:
   forall chunk m1 b ofs v m2 chunk' ofs' v',
   store chunk m1 b ofs v = Some m2 ->