From b27d386185527d1ee9d0bb77ebe3bacffc2bf05a Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 5 Apr 2019 00:12:45 +0200 Subject: factor out some proofs --- mppa_k1c/Asmblockgenproof1.v | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) (limited to 'mppa_k1c') 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. -- cgit