1 files changed, 0 insertions, 18 deletions
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index 7d557c6d..84e1e5bb 100644
--- a/powerpc/ConstpropOpproof.v
+++ b/powerpc/ConstpropOpproof.v
@@ -430,24 +430,6 @@ Proof.
   auto.
 Qed.
 
-Lemma builtin_strength_reduction_correct:
-  forall ef args vl m t vres m',
-  vl = approx_regs app args ->
-  external_call ef ge rs##args m t vres m' ->
-  let (ef', args') := builtin_strength_reduction ef args vl in
-  external_call ef' ge rs##args' m t vres m'.
-Proof.
-  intros until m'. unfold builtin_strength_reduction.
-  destruct (builtin_strength_reduction_match ef args vl); simpl; intros; InvApproxRegs; SimplVMA.
-  unfold symbol_address in H. destruct (Genv.find_symbol ge symb) as [b|] eqn:?; rewrite H in H0.
-  rewrite volatile_load_global_charact. exists b; auto. 
-  inv H0.
-  unfold symbol_address in H1. destruct (Genv.find_symbol ge symb) as [b|] eqn:?; rewrite H1 in H0.
-  rewrite volatile_store_global_charact. exists b; auto. 
-  inv H0.
-  auto.
-Qed.
-
 End STRENGTH_REDUCTION.
 
 End ANALYSIS.