diff options
Diffstat (limited to 'backend/CSEproof.v')
| -rw-r--r-- | backend/CSEproof.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 317fb82..af138f8 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -497,7 +497,6 @@ Proof. - inv H. rewrite is_uns_zero_ext in H3 by omega. rewrite H3; auto. - inv H. rewrite is_sgn_sign_ext in H3 by omega. rewrite H3; auto. - inv H. rewrite is_uns_zero_ext in H3 by omega. rewrite H3; auto. -- inv H. rewrite Float.singleoffloat_of_single by auto. auto. Qed. Lemma add_store_result_hold: |