diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-20 06:35:43 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-20 06:35:43 +0100 |
| commit | b1b2c6c6442a48c8eb2f7f378e440d8d4311048f (patch) | |
| tree | df7531b43cc34781edb60f070fb3e1fc72b5f44f /mppa_k1c | |
| parent | 5e05d4acc53b4b098cb55006b8daa32149d7fba4 (diff) | |
| download | compcert-kvx-b1b2c6c6442a48c8eb2f7f378e440d8d4311048f.tar.gz compcert-kvx-b1b2c6c6442a48c8eb2f7f378e440d8d4311048f.zip | |
proof clarification
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 4c29867b..00df01e3 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1483,6 +1483,8 @@ Proof. destruct (Z_lt_dec _ _); destruct (Z.eq_dec _ _); trivial; omega. Qed. +Ltac splitall := repeat match goal with |- _ /\ _ => split end. + Lemma transl_op_correct: forall op args res k (rs: regset) m v c, transl_op op args res k = OK c -> @@ -1575,7 +1577,7 @@ Opaque Int.eq. all: destruct c. all: simpl in *. all: inv EQ2. - all: try (econstructor; split; [idtac | split ]). + all: econstructor; splitall. all: try apply exec_straight_one. all: intros; simpl; trivial. all: unfold Val.select, cmove, cmoveu; simpl. @@ -1599,7 +1601,7 @@ Opaque Int.eq. all: destruct c. all: simpl in *. all: inv EQ0. - all: try (econstructor; split; [idtac | split ]). + all: econstructor; splitall. all: try apply exec_straight_one. all: intros; simpl; trivial. all: unfold Val.select, cmove, cmoveu; simpl. @@ -1623,7 +1625,7 @@ Opaque Int.eq. all: destruct c. all: simpl in *. all: inv EQ0. - all: try (econstructor; split; [idtac | split ]). + all: econstructor; splitall. all: try apply exec_straight_one. all: intros; simpl; trivial. all: unfold Val.select, cmove, cmoveu; simpl. |