diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-02-22 16:57:02 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-04 16:30:06 +0200 |
| commit | f1d3dbb3fa70233d1ad83ae88876dd384346a16a (patch) | |
| tree | 356dd54e5ae0a960eaa60a7b174ceb4fa750f9fc /mppa_k1c/Asmgenproof1.v | |
| parent | 6a3f3a62452670380827f9e39dd28c5092741099 (diff) | |
| download | compcert-kvx-f1d3dbb3fa70233d1ad83ae88876dd384346a16a.tar.gz compcert-kvx-f1d3dbb3fa70233d1ad83ae88876dd384346a16a.zip | |
Changed ptr64 to be always true
Diffstat (limited to 'mppa_k1c/Asmgenproof1.v')
| -rw-r--r-- | mppa_k1c/Asmgenproof1.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mppa_k1c/Asmgenproof1.v b/mppa_k1c/Asmgenproof1.v index 7f070c12..8bbdbd4c 100644 --- a/mppa_k1c/Asmgenproof1.v +++ b/mppa_k1c/Asmgenproof1.v @@ -553,9 +553,9 @@ Lemma transl_cond_int32s_correct: Proof. intros. destruct cmp; simpl. - econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. destruct (rs##r1); auto. destruct (rs##r2); auto. + split; intros; Simpl. destruct (rs##r1); auto. - econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. destruct (rs##r1); auto. destruct (rs##r2); auto. + split; intros; Simpl. destruct (rs##r1); auto. - econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. split; intros; Simpl. - econstructor; split. |