From 7ea8a55692e2a2d32efa0c84e19c37a3b56a0fd1 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 19 Aug 2011 09:13:09 +0000
Subject: Cleaned up old commented-out parts

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1719 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 powerpc/Asmgenproof.v | 8 --------
 1 file changed, 8 deletions(-)

(limited to 'powerpc/Asmgenproof.v')

diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index d22bc3d6..27b2108b 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -114,14 +114,6 @@ Proof.
   eauto.
 Qed.
 
-(*
-Remark code_size_pos:
-  forall fn, code_size fn >= 0.
-Proof.
-  induction fn; simpl; omega.
-Qed.
-*)
-
 Remark code_tail_bounds:
   forall fn ofs i c,
   code_tail ofs fn (i :: c) -> 0 <= ofs < list_length_z fn.
-- 
cgit