summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--arm/Asmgenproof1.v2
-rw-r--r--arm/SelectOp.vp2
-rw-r--r--powerpc/Asmgenproof1.v4
3 files changed, 0 insertions, 8 deletions
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index 1e65d72..ec6d405 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -1216,7 +1216,6 @@ Proof.
eapply transl_load_int_correct; eauto.
discriminate.
eapply transl_load_float_correct; eauto.
- apply Mem.loadv_float64al32 in H1. eapply transl_load_float_correct; eauto.
eapply transl_load_float_correct; eauto.
Qed.
@@ -1246,7 +1245,6 @@ Proof.
simpl. unfold exec_store. rewrite H. rewrite H2; eauto with asmgen.
rewrite H1. eauto. auto. intros. Simpl.
simpl; auto.
-- apply Mem.storev_float64al32 in H1. eapply transl_store_float_correct; eauto.
- eapply transl_store_float_correct; eauto.
Qed.
diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index 767e747..2b0bdff 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -401,7 +401,6 @@ Definition can_use_Aindexed2 (chunk: memory_chunk): bool :=
| Mint64 => false
| Mfloat32 => false
| Mfloat64 => false
- | Mfloat64al32 => false
end.
Definition can_use_Aindexed2shift (chunk: memory_chunk): bool :=
@@ -414,7 +413,6 @@ Definition can_use_Aindexed2shift (chunk: memory_chunk): bool :=
| Mint64 => false
| Mfloat32 => false
| Mfloat64 => false
- | Mfloat64al32 => false
end.
Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index e637ef8..2436e2f 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -1161,8 +1161,6 @@ Proof.
- (* Mfloat32 *)
eapply BASE; eauto; erewrite freg_of_eq by eauto; auto.
- (* Mfloat64 *)
- apply Mem.loadv_float64al32 in H1. eapply BASE; eauto; erewrite freg_of_eq by eauto; auto.
-- (* Mfloat64al32 *)
eapply BASE; eauto; erewrite freg_of_eq by eauto; auto.
Qed.
@@ -1235,8 +1233,6 @@ Local Transparent destroyed_by_store.
simpl. unfold store2. rewrite H. rewrite H2; auto with asmgen. rewrite H1. eauto. auto.
simpl; intros. destruct H5 as [A [B C]]. Simpl. apply H2; auto with asmgen. destruct TEMP0; congruence.
- (* Mfloat64 *)
- apply Mem.storev_float64al32 in H1. eapply BASE; eauto; erewrite freg_of_eq by eauto; auto.
-- (* Mfloat64al32 *)
eapply BASE; eauto; erewrite freg_of_eq by eauto; auto.
Qed.