diff options
Diffstat (limited to 'powerpc/Asmgenproof.v')
| -rw-r--r-- | powerpc/Asmgenproof.v | 8 |
1 files changed, 0 insertions, 8 deletions
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. |