Val_cmp* -> Val.mxcmp*

1 files changed, 6 insertions, 21 deletions

diff --git a/scheduling/postpass_lib/Machblockgenproof.v b/scheduling/postpass_lib/Machblockgenproof.v
index fc722887..d121a54b 100644
--- a/scheduling/postpass_lib/Machblockgenproof.v
+++ b/scheduling/postpass_lib/Machblockgenproof.v
@@ -190,7 +190,7 @@ Proof.
   intros H H0 H1.
   unfold find_label.
   remember (is_label l _) as b.
-  cutrewrite (b = false); auto.
+  replace b with false; auto.
   subst; unfold is_label.
   destruct i; cbn in * |- *; try (destruct (in_dec l nil); intuition).
   inversion H.
@@ -286,7 +286,7 @@ Lemma find_label_preserved:
   Mach.find_label l (Mach.fn_code f) = Some c ->
   exists h, In l h /\ find_label l (fn_code (transf_function f)) = Some (concat h (trans_code c)).
 Proof.
-  intros. cutrewrite ((fn_code (transf_function f)) = trans_code (Mach.fn_code f)); eauto.
+  intros. replace (fn_code (transf_function f)) with (trans_code (Mach.fn_code f)); eauto.
   apply find_label_transcode_preserved; auto.
 Qed.
 
@@ -661,7 +661,7 @@ Proof.
     inversion H1; subst; clear H1.
     inversion_clear H0; cbn.
     - (* function_internal*)
-      cutrewrite (trans_code (Mach.fn_code f0) = fn_code (transf_function f0)); eauto.
+      replace (trans_code (Mach.fn_code f0)) with (fn_code (transf_function f0)); eauto.
       eapply exec_function_internal; eauto.
       rewrite <- parent_sp_preserved; eauto.
       rewrite <- parent_ra_preserved; eauto.
@@ -733,12 +733,12 @@ Proof.
   intro H; destruct c as [|i' c]. { inversion H. }
   remember (trans_inst i) as ti.
   destruct ti as [lbl|bi|cfi].
-  - (*i=lbl *) cutrewrite (i = Mlabel lbl). 2: ( destruct i; cbn in * |- *; try congruence ).
+  - (*i=lbl *) replace (i ) with (Mlabel lbl). 2: ( destruct i; cbn in * |- *; try congruence ).
     exists nil; cbn; eexists. eapply Tr_add_label; eauto.
   - (*i=basic*)
     destruct i'.
     10: { exists (add_to_new_bblock (MB_basic bi)::nil).  exists b. 
-      cutrewrite ((add_to_new_bblock (MB_basic bi) :: nil) ++ (b::l)=(add_to_new_bblock (MB_basic bi) :: (b::l)));eauto.
+      replace ((add_to_new_bblock (MB_basic bi) :: nil) ++ (b::l)) with ((add_to_new_bblock (MB_basic bi) :: (b::l)));eauto.
       rewrite Heqti.        
       eapply  Tr_end_block; eauto.
       rewrite <-Heqti.
@@ -748,7 +748,7 @@ Proof.
   - (*i=cfi*)
     destruct i; try(cbn in Heqti; congruence).
     all: exists (add_to_new_bblock (MB_cfi cfi)::nil);  exists b; 
-        cutrewrite ((add_to_new_bblock (MB_cfi cfi) :: nil) ++ (b::l)=(add_to_new_bblock (MB_cfi cfi) :: (b::l)));eauto;
+        replace ((add_to_new_bblock (MB_cfi cfi) :: nil) ++ (b::l)) with ((add_to_new_bblock (MB_cfi cfi) :: (b::l)));eauto;
         rewrite Heqti;        
         eapply  Tr_end_block; eauto;
         rewrite <-Heqti;
@@ -765,21 +765,6 @@ Proof.
     eauto.
 Qed.
 
-(* FIXME: these two lemma should go into [Coqlib.v] *) 
-Lemma is_tail_app A (l1: list A): forall l2, is_tail l2 (l1 ++ l2).
-Proof.
-  induction l1; cbn; auto with coqlib.
-Qed.
-Hint Resolve is_tail_app: coqlib.
-
-Lemma is_tail_app_inv A (l1: list A): forall l2 l3, is_tail (l1 ++ l2) l3 -> is_tail l2 l3.
-Proof.
-  induction l1; cbn; auto with coqlib.
-  intros l2 l3 H; inversion H; eauto with coqlib.
-Qed.
-Hint Resolve is_tail_app_inv: coqlib.
-
-
 Lemma Mach_Machblock_tail sg ros c c1 c2: c1=(Mcall sg ros :: c) -> is_tail c1 c2 -> 
   exists b, is_tail (b :: trans_code c) (trans_code c2).
 Proof.