From fdcaf6fabd3d594e40a2b7a31341202e9a93f5cb Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 7 Mar 2012 09:22:56 +0000 Subject: PowerPC: remove the fmadd and fmsub operators/Asm instructions (definitely not semantics-preserving; hard to justify). CPragmas: make sure SDAs are not recognized on MacOSX. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1836 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/SelectOpproof.v | 15 ++------------- 1 file changed, 2 insertions(+), 13 deletions(-) (limited to 'powerpc/SelectOpproof.v') diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 1d35d9f8..27a0fd01 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -631,23 +631,12 @@ Qed. Theorem eval_addf: binary_constructor_sound addf Val.addf. Proof. - red; intros until y; unfold addf. - destruct (use_fused_mul tt); simpl. - case (addf_match a b); intros; InvEval. - TrivialExists. simpl. congruence. - TrivialExists. simpl. rewrite Val.addf_commut. congruence. - intros. TrivialExists. - intros. TrivialExists. + red; intros; TrivialExists. Qed. Theorem eval_subf: binary_constructor_sound subf Val.subf. Proof. - red; intros until y; unfold subf. - destruct (use_fused_mul tt); simpl. - case (subf_match a); intros; InvEval. - TrivialExists. simpl. congruence. - TrivialExists. - intros. TrivialExists. + red; intros; TrivialExists. Qed. Theorem eval_mulf: binary_constructor_sound mulf Val.mulf. -- cgit