diff options
Diffstat (limited to 'scheduling/Parallelizability.v')
| -rw-r--r-- | scheduling/Parallelizability.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/scheduling/Parallelizability.v b/scheduling/Parallelizability.v index e5d21434..afa4b9fd 100644 --- a/scheduling/Parallelizability.v +++ b/scheduling/Parallelizability.v @@ -299,7 +299,7 @@ Proof. induction i as [|[y e] i']; cbn. - intros m tmp H x H0; inversion_clear H; auto. - intros m tmp H x (H1 & H2); destruct (exp_eval ge e tmp old); cbn; try congruence. - cutrewrite (m x = assign m y v x); eauto. + replace (m x) with (assign m y v x); eauto. rewrite assign_diff; auto. Qed. @@ -514,13 +514,13 @@ Proof. induction i as [|[x e] i']; cbn; auto. intros m tmp1 tmp2; rewrite disjoint_cons_l, disjoint_app_l. intros (H1 & H2 & H3) H6 H7. - cutrewrite (exp_eval ge e tmp1 old1 = exp_eval ge e tmp2 old2). + replace (exp_eval ge e tmp1 old1) with (exp_eval ge e tmp2 old2). - destruct (exp_eval ge e tmp2 old2); auto. eapply IHi'; eauto. cbn; intros x0 H0; unfold assign. destruct (R.eq_dec x x0); cbn; auto. - unfold disjoint in H2; apply exp_frame_correct. - intros;apply H6; auto. - intros;apply H7; auto. + intros;rewrite H6; auto. + intros;rewrite H7; auto. Qed. (** * Parallelizability *) |