Cleaned up old commented-out parts

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1719 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 0 insertions, 24 deletions

diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v
index c00332e..be40f3d 100644
--- a/ia32/Asmgenproof1.v
+++ b/ia32/Asmgenproof1.v
@@ -232,30 +232,6 @@ Qed.
 
 Hint Resolve nontemp_diff: ppcgen.
 
-(*
-Remark undef_regs_1:
-  forall l ms r, ms r = Vundef -> Mach.undef_regs l ms r = Vundef.
-Proof.
-  induction l; simpl; intros. auto. apply IHl. unfold Regmap.set.
-  destruct (RegEq.eq r a); congruence.
-Qed.
-
-Remark undef_regs_2:
-  forall l ms r, In r l -> Mach.undef_regs l ms r = Vundef.
-Proof.
-  induction l; simpl; intros. contradiction. 
-  destruct H. subst. apply undef_regs_1. apply Regmap.gss.
-  auto.
-Qed.
-
-Remark undef_regs_3:
-  forall l ms r, ~In r l -> Mach.undef_regs l ms r = ms r.
-Proof.
-  induction l; simpl; intros. auto.
-  rewrite IHl. apply Regmap.gso. intuition. intuition.
-Qed.
-*)
-
 Lemma agree_exten_temps:
   forall ms sp rs rs',
   agree ms sp rs ->