summaryrefslogtreecommitdiff
path: root/powerpc
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2011-08-19 09:13:09 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2011-08-19 09:13:09 +0000
commit7ea8a55692e2a2d32efa0c84e19c37a3b56a0fd1 (patch)
treee324aff1a958e0a5d83f805ff3ca1d9eb07939f4 /powerpc
parent5b73a4f223a0cadb7df3f1320fed86cde0d67d6e (diff)
Cleaned up old commented-out parts
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1719 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc')
-rw-r--r--powerpc/Asmgenproof.v8
-rw-r--r--powerpc/Asmgenproof1.v10
2 files changed, 0 insertions, 18 deletions
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index d22bc3d..27b2108 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.
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index 42355ad..0b7f4d0 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -559,16 +559,6 @@ Qed.
(** * Correctness of PowerPC constructor functions *)
-(*
-Ltac SIMP :=
- match goal with
- | [ |- nextinstr _ _ = _ ] => rewrite nextinstr_inv; [auto | auto with ppcgen]
- | [ |- Pregmap.get ?x (Pregmap.set ?x _ _) = _ ] => rewrite Pregmap.gss; auto
- | [ |- Pregmap.set ?x _ _ ?x = _ ] => rewrite Pregmap.gss; auto
- | [ |- Pregmap.get _ (Pregmap.set _ _ _) = _ ] => rewrite Pregmap.gso; [auto | auto with ppcgen]
- | [ |- Pregmap.set _ _ _ _ = _ ] => rewrite Pregmap.gso; [auto | auto with ppcgen]
- end.
-*)
Ltac SIMP :=
(rewrite nextinstr_inv || rewrite Pregmap.gss || rewrite Pregmap.gso); auto with ppcgen.