diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2020-04-01 10:35:16 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2020-04-01 10:35:16 +0200 |
| commit | 027c5f9b643c554bef742bf907e725f8ad949429 (patch) | |
| tree | b5a6cd23042a1d396c30debde60f92eca8cca7d2 | |
| parent | c974b25682251da237dbbe8ef3af218c6d175ae2 (diff) | |
| download | compcert-kvx-027c5f9b643c554bef742bf907e725f8ad949429.tar.gz compcert-kvx-027c5f9b643c554bef742bf907e725f8ad949429.zip | |
Fix cutrewrite deprecated
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 3b123c75..8cc7f0ab 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -61,9 +61,9 @@ Proof. - subst. repeat (rewrite Pregmap.gss); auto. destruct v; simpl; auto. rewrite Ptrofs.add_assoc. - cutrewrite (Ptrofs.repr (x + y) = Ptrofs.add (Ptrofs.repr x) (Ptrofs.repr y)); auto. + enough (Ptrofs.repr (x + y) = Ptrofs.add (Ptrofs.repr x) (Ptrofs.repr y)) as ->; auto. unfold Ptrofs.add. - cutrewrite (x + y = Ptrofs.unsigned (Ptrofs.repr x) + Ptrofs.unsigned (Ptrofs.repr y)); auto. + enough (x + y = Ptrofs.unsigned (Ptrofs.repr x) + Ptrofs.unsigned (Ptrofs.repr y)) as ->; auto. repeat (rewrite Ptrofs.unsigned_repr); auto. - repeat (rewrite Pregmap.gso; auto). Qed. @@ -220,7 +220,8 @@ Proof. destruct (zeq pos 0). + inv H. exists lbb. constructor; auto. + apply IHlbb in H. destruct H as (c & TAIL). exists c. - cutrewrite (pos = pos - size a + size a). apply code_tail_S; auto. + enough (pos = pos - size a + size a) as ->. + apply code_tail_S; auto. omega. Qed. |