diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-04-05 18:14:07 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-04-05 18:14:07 +0200 |
| commit | fb8c244726595b0e7a4db8c0f8e6aa3f3549cc14 (patch) | |
| tree | 418bdade1b8dba8682b1d2fd0b1e36294f7cd9ad /mppa_k1c/lib | |
| parent | 9d94664fa180d909c43992a4cbdf6808fb9c4289 (diff) | |
| download | compcert-kvx-fb8c244726595b0e7a4db8c0f8e6aa3f3549cc14.tar.gz compcert-kvx-fb8c244726595b0e7a4db8c0f8e6aa3f3549cc14.zip | |
relecture sylvain
avec TODOs pour refactoring #90
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 8a83521c..fa920a8c 100644 --- a/mppa_k1c/lib/Asmblockgenproof0.v +++ b/mppa_k1c/lib/Asmblockgenproof0.v @@ -1006,7 +1006,7 @@ Lemma exec_straight_through_singleinst: Proof. intros. subst. constructor 1. unfold exec_bblock. simpl body. erewrite exec_straight_body; eauto. simpl. 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. (** The following lemmas show that straight-line executions |