1 files changed, 31 insertions, 2 deletions

diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v
index 53ecf73a..f6f03868 100644
--- a/backend/Asmgenproof0.v
+++ b/backend/Asmgenproof0.v
@@ -103,7 +103,7 @@ Lemma nextinstr_set_preg:
   (nextinstr (rs#(preg_of m) <- v))#PC = Val.offset_ptr rs#PC Ptrofs.one.
 Proof.
   intros. unfold nextinstr. rewrite Pregmap.gss.
-  rewrite Pregmap.gso. auto. apply sym_not_eq. apply preg_of_not_PC.
+  rewrite Pregmap.gso. auto. apply not_eq_sym. apply preg_of_not_PC.
 Qed.
 
 Lemma undef_regs_other:
@@ -211,7 +211,7 @@ Lemma agree_set_mreg:
   agree (Regmap.set r v ms) sp rs'.
 Proof.
   intros. destruct H. split; auto.
-  rewrite H1; auto. apply sym_not_equal. apply preg_of_not_SP.
+  rewrite H1; auto. apply not_eq_sym. apply preg_of_not_SP.
   intros. unfold Regmap.set. destruct (RegEq.eq r0 r). congruence.
   rewrite H1. auto. apply preg_of_data.
   red; intros; elim n. eapply preg_of_injective; eauto.
@@ -285,6 +285,23 @@ Proof.
   exploit preg_of_injective; eauto. congruence.
 Qed.
 
+Lemma agree_undef_regs2:
+  forall ms sp rl rs rs',
+  agree (Mach.undef_regs rl ms) sp rs ->
+  (forall r', data_preg r' = true -> preg_notin r' rl -> rs'#r' = rs#r') ->
+  agree (Mach.undef_regs rl ms) sp rs'.
+Proof.
+  intros. destruct H. split; auto.
+  rewrite <- agree_sp0. apply H0; auto.
+  rewrite preg_notin_charact. intros. apply not_eq_sym. apply preg_of_not_SP.
+  intros. destruct (In_dec mreg_eq r rl).
+  rewrite Mach.undef_regs_same; auto.
+  rewrite H0; auto.
+  apply preg_of_data.
+  rewrite preg_notin_charact. intros; red; intros. elim n.
+  exploit preg_of_injective; eauto. congruence.
+Qed.
+
 Lemma agree_set_undef_mreg:
   forall ms sp rs r v rl rs',
   agree ms sp rs ->
@@ -738,6 +755,18 @@ Ltac TailNoLabel :=
   | _ => idtac
   end.
 
+Remark tail_nolabel_find_label:
+  forall lbl k c, tail_nolabel k c -> find_label lbl c = find_label lbl k.
+Proof.
+  intros. destruct H. auto.
+Qed.
+
+Remark tail_nolabel_is_tail:
+  forall k c, tail_nolabel k c -> is_tail k c.
+Proof.
+  intros. destruct H. auto.
+Qed.
+
 (** * Execution of straight-line code *)
 
 Section STRAIGHTLINE.