- Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.

- Revised printing of intermediate RTL code.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2403 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 5 insertions, 1 deletions

diff --git a/common/Memory.v b/common/Memory.v
index 0260a895..9afdfd39 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -727,6 +727,7 @@ Proof.
   rewrite pred_dec_false; auto.
 Qed.
 
+(*
 Theorem load_float64al32:
   forall m b ofs v,
   load Mfloat64 m b ofs = Some v -> load Mfloat64al32 m b ofs = Some v.
@@ -742,6 +743,7 @@ Theorem loadv_float64al32:
 Proof.
   unfold loadv; intros. destruct a; auto. apply load_float64al32; auto.
 Qed.
+*)
 
 (** ** Properties related to [loadbytes] *)
 
@@ -1411,6 +1413,7 @@ Proof.
   auto.
 Qed.
 
+(*
 Theorem store_float64al32:
   forall m b ofs v m',
   store Mfloat64 m b ofs v = Some m' -> store Mfloat64al32 m b ofs v = Some m'.
@@ -1428,6 +1431,7 @@ Theorem storev_float64al32:
 Proof.
   unfold storev; intros. destruct a; auto. apply store_float64al32; auto.
 Qed.
+*)
 
 (** ** Properties related to [storebytes]. *)
 
@@ -3422,7 +3426,7 @@ Proof.
     destruct H0. subst; exists Mint8unsigned; auto.
     destruct H0. subst; exists Mint16unsigned; auto.
     destruct H0. subst; exists Mint32; auto.
-    subst; exists Mfloat64; auto.
+    subst; exists Mint64; auto.
   destruct R as [chunk [A B]].
   assert (valid_access m chunk b ofs Nonempty).
     split. red; intros; apply H3. omega. congruence.