From 7ea8a55692e2a2d32efa0c84e19c37a3b56a0fd1 Mon Sep 17 00:00:00 2001 From: xleroy 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 --- ia32/Asmgenproof1.v | 24 ------------------------ 1 file changed, 24 deletions(-) (limited to 'ia32/Asmgenproof1.v') diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index c00332ed..be40f3d4 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 -> -- cgit