diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-05 00:12:45 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-05 00:12:45 +0200 |
| commit | b27d386185527d1ee9d0bb77ebe3bacffc2bf05a (patch) | |
| tree | 5b634dd4056d1612a5c363b65bcab260ba5ac469 /mppa_k1c/Asmblockgenproof1.v | |
| parent | a4f081bd7972c9007104942bdf90a4042397e167 (diff) | |
| download | compcert-kvx-b27d386185527d1ee9d0bb77ebe3bacffc2bf05a.tar.gz compcert-kvx-b27d386185527d1ee9d0bb77ebe3bacffc2bf05a.zip | |
factor out some proofs
Diffstat (limited to 'mppa_k1c/Asmblockgenproof1.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index e58c7f0c..7da86de4 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1639,10 +1639,9 @@ Opaque Int.eq. exists rs'; split. eexact A. eauto with asmgen. - (* Oselect *) destruct cond in *; simpl in *; try congruence; injection EQ3; clear EQ3; intro Hrew; rewrite <- Hrew in *; - econstructor; split. - - + eapply exec_straight_one. - simpl; reflexivity. + econstructor; split; + try ( eapply exec_straight_one; + simpl; reflexivity ). + split. * unfold eval_select. destruct (rs x) eqn:eqX; try constructor. @@ -1652,8 +1651,6 @@ Opaque Int.eq. destruct b; simpl; rewrite Pregmap.gss; constructor. * intros. rewrite Pregmap.gso; congruence. - + eapply exec_straight_one. - simpl; reflexivity. + split. * unfold eval_select. destruct (rs x) eqn:eqX; try constructor. |