diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-20 21:12:35 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-20 21:12:35 +0200 |
| commit | 69010f52e11859619c0894f91cdb5840eb4986aa (patch) | |
| tree | 2e1039fedfeeb9e8176d7c72baacc74442229971 | |
| parent | 7b0089ab6de94f81021c5c3d78aea752d2582253 (diff) | |
| download | compcert-kvx-69010f52e11859619c0894f91cdb5840eb4986aa.tar.gz compcert-kvx-69010f52e11859619c0894f91cdb5840eb4986aa.zip | |
detail with shrxl
| -rw-r--r-- | mppa_k1c/ConstpropOpproof.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/mppa_k1c/ConstpropOpproof.v b/mppa_k1c/ConstpropOpproof.v index ae11a220..4dd0441d 100644 --- a/mppa_k1c/ConstpropOpproof.v +++ b/mppa_k1c/ConstpropOpproof.v @@ -276,7 +276,8 @@ Proof. inv H; auto. destruct (Int.is_power2 n) eqn:?. destruct (Int.ltu i (Int.repr 31)) eqn:?. - exists v; split; auto. simpl. eapply Val.divs_pow2; eauto. congruence. + exists v; split; auto. simpl. + erewrite Val.divs_pow2; eauto. reflexivity. congruence. exists v; auto. exists v; auto. Qed. @@ -449,7 +450,8 @@ Lemma make_divlimm_correct: Proof. intros; unfold make_divlimm. destruct (Int64.is_power2' n) eqn:?. destruct (Int.ltu i (Int.repr 63)) eqn:?. - rewrite H0 in H. econstructor; split. simpl; eauto. eapply Val.divls_pow2; eauto. auto. + rewrite H0 in H. econstructor; split. simpl; eauto. + erewrite Val.divls_pow2; eauto. auto. exists v; auto. exists v; auto. Qed. |