From f2d0caa5f7594cf936713f3bd6cdc3ab5a6f9626 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Thu, 31 Jul 2014 07:33:53 +0000
Subject: Add Mem.free_parallel_inject and use it to simplify Events a bit.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2556 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 common/Memtype.v | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'common/Memtype.v')

diff --git a/common/Memtype.v b/common/Memtype.v
index 1ab1cb73..d94c895f 100644
--- a/common/Memtype.v
+++ b/common/Memtype.v
@@ -1177,6 +1177,15 @@ Axiom free_inject:
     exists lo1, exists hi1, In (b1, lo1, hi1) l /\ lo1 <= ofs < hi1) ->
   inject f m1' m2'.
 
+Axiom free_parallel_inject:
+  forall f m1 m2 b lo hi m1' b' delta,
+  inject f m1 m2 ->
+  free m1 b lo hi = Some m1' ->
+  f b = Some(b', delta) ->
+  exists m2',
+     free m2 b' (lo + delta) (hi + delta) = Some m2'
+  /\ inject f m1' m2'.
+
 Axiom drop_outside_inject:
   forall f m1 m2 b lo hi p m2',
   inject f m1 m2 -> 
-- 
cgit