From 7ea8a55692e2a2d32efa0c84e19c37a3b56a0fd1 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 19 Aug 2011 09:13:09 +0000
Subject: Cleaned up old commented-out parts

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1719 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 common/Determinism.v | 19 -------------------
 common/Events.v      | 21 ---------------------
 common/Memdata.v     |  8 --------
 common/Memory.v      | 10 ----------
 4 files changed, 58 deletions(-)

(limited to 'common')

diff --git a/common/Determinism.v b/common/Determinism.v
index 29cc695..778ba22 100644
--- a/common/Determinism.v
+++ b/common/Determinism.v
@@ -126,25 +126,6 @@ Proof.
   inv H4; inv H3. inv H7; inv H6. auto.
 Qed.
 
-(*
-Lemma possible_event_final_world:
-  forall w ev w1 w2,
-  possible_event w ev w1 -> possible_event w ev w2 -> w1 = w2.
-Proof.
-  intros. inv H; inv H0; congruence.
-Qed.
-
-Lemma possible_trace_final_world:
-  forall w0 t w1, possible_trace w0 t w1 ->
-  forall w2, possible_trace w0 t w2 -> w1 = w2.
-Proof.
-  induction 1; intros.
-  inv H. auto.
-  inv H1. assert (w2 = w5) by (eapply possible_event_final_world; eauto). 
-  subst; eauto.
-Qed.
-*)
-
 CoInductive possible_traceinf: world -> traceinf -> Prop :=
   | possible_traceinf_cons: forall w1 ev w2 T,
       possible_event w1 ev w2 ->
diff --git a/common/Events.v b/common/Events.v
index 3948640..f18c091 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -1044,18 +1044,6 @@ Proof.
   intros. inv H. 
   inv H1. inv H13. inv H14. inv H10. inv H11.
   exploit Mem.loadbytes_length; eauto. intros LEN.
-(*
-  destruct (zle sz 0).
-  (* empty copy *)
-  rewrite nat_of_Z_neg in LEN; auto. 
-  assert (bytes = nil). destruct bytes; simpl in LEN; congruence.
-  subst. rewrite Mem.storebytes_empty in H8. inv H8.
-  exists Vundef; exists m1'.
-  split. econstructor; eauto. rewrite Mem.loadbytes_empty; eauto. 
-  apply Mem.storebytes_empty. 
-  split. constructor. split. auto. red; auto.
-  (* nonempty copy *)
-*)
   exploit Mem.loadbytes_extends; eauto. intros [bytes2 [A B]].
   exploit Mem.storebytes_within_extends; eauto. intros [m2' [C D]].
   exists Vundef; exists m2'.
@@ -1079,15 +1067,6 @@ Proof.
 (* injections *)
   intros. inv H0. inv H2. inv H14. inv H15. inv H11. inv H12.
   exploit Mem.loadbytes_length; eauto. intros LEN.
-(*
-  destruct (zle sz 0).
-  (* empty copy *)
-  rewrite nat_of_Z_neg in LEN; auto. 
-  assert (bytes = nil). destruct bytes; simpl in LEN; congruence.
-  subst. rewrite Mem.storebytes_empty in H9. inv H9.
-  exists f; exists Vundef; exists m1'.
-  split. econstructor; eauto. 
-*)
   assert (RPSRC: Mem.range_perm m1 bsrc (Int.unsigned osrc) (Int.unsigned osrc + sz) Nonempty).
     eapply Mem.range_perm_implies. eapply Mem.loadbytes_range_perm; eauto. auto with mem.
   assert (RPDST: Mem.range_perm m1 bdst (Int.unsigned odst) (Int.unsigned odst + sz) Nonempty).
diff --git a/common/Memdata.v b/common/Memdata.v
index 16adb23..fde8b47 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -534,14 +534,6 @@ Definition decode_val (chunk: memory_chunk) (vl: list memval) : val :=
       end
   end.
 
-(*
-Lemma inj_pointer_length:
-  forall b ofs n, List.length(inj_pointer n b ofs) = n.
-Proof.
-  induction n; simpl; congruence.
-Qed.
-*)
-
 Lemma encode_val_length:
   forall chunk v, length(encode_val chunk v) = size_chunk_nat chunk.
 Proof.
diff --git a/common/Memory.v b/common/Memory.v
index b456191..157867e 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -947,16 +947,6 @@ Variable ofs: Z.
 Variable v: val.
 Variable m2: mem.
 Hypothesis STORE: store chunk m1 b ofs v = Some m2.
-(*
-Lemma store_result:
-  m2 = unchecked_store chunk m1 b ofs v.
-Proof.
-  unfold store in STORE.
-  destruct (valid_access_dec m1 chunk b ofs Writable).
-  congruence. 
-  congruence.
-Qed.
-*)
 
 Lemma store_access: mem_access m2 = mem_access m1.
 Proof.
-- 
cgit v1.2.3