From 0053b1aa1d26da5d1f995a603b127daf799c2da9 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 21 May 2012 16:26:30 +0000
Subject: Merge of the newmem branch: - Revised memory model with Max and Cur
 permissions, but without bounds - Constant propagation of 'const' globals -
 Function inlining at RTL level - (Unprovable) elimination of unreferenced
 static definitions

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 cfrontend/Initializersproof.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'cfrontend/Initializersproof.v')

diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index 627db890..37f15cfe 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -327,8 +327,8 @@ Qed.
 Lemma mem_empty_not_valid_pointer:
   forall b ofs, Mem.valid_pointer Mem.empty b ofs = false.
 Proof.
-  intros. unfold Mem.valid_pointer. destruct (Mem.perm_dec Mem.empty b ofs Nonempty); auto.
-  red in p. simpl in p. contradiction.
+  intros. unfold Mem.valid_pointer. destruct (Mem.perm_dec Mem.empty b ofs Cur Nonempty); auto.
+  eelim Mem.perm_empty; eauto. 
 Qed.
 
 Lemma sem_cmp_match:
-- 
cgit