diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-04-08 11:20:12 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-04-08 11:20:12 +0200 |
| commit | 5cb91df0e3faaca529798e14edb9c39046b27767 (patch) | |
| tree | c0f00ffd735f38fb9d2c79d6367fae2d07ec89dc /mppa_k1c/lib | |
| parent | 76af54d8ae77f843b7f6f15f9a0fc6124df47ebb (diff) | |
| parent | fb8c244726595b0e7a4db8c0f8e6aa3f3549cc14 (diff) | |
| download | compcert-kvx-5cb91df0e3faaca529798e14edb9c39046b27767.tar.gz compcert-kvx-5cb91df0e3faaca529798e14edb9c39046b27767.zip | |
Merge remote-tracking branch 'origin/mppa-refactor-reviewed' into mppa-refactor
Conflicts:
mppa_k1c/Asmblock.v
mppa_k1c/Asmblockdeps.v
mppa_k1c/PostpassSchedulingproof.v
mppa_k1c/lib/Asmblockgenproof0.v
Diffstat (limited to 'mppa_k1c/lib')
| -rw-r--r-- | mppa_k1c/lib/Asmblockgenproof0.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v index a44c40d8..eb336edc 100644 --- a/mppa_k1c/lib/Asmblockgenproof0.v +++ b/mppa_k1c/lib/Asmblockgenproof0.v @@ -1014,7 +1014,7 @@ Lemma exec_straight_through_singleinst: Proof. intros. subst. constructor 1. unfold exec_bblock. simpl body. erewrite exec_straight_body; eauto. simpl. rewrite regset_same_assign. auto. - simpl; auto. unfold nextblock; simpl. Simpl. erewrite exec_straight_pc; eauto. + simpl; auto. unfold nextblock, incrPC; simpl. Simpl. erewrite exec_straight_pc; eauto. Qed. |