diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-10-29 21:56:59 +0200 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-10-29 21:56:59 +0200 |
| commit | ae2d228c04f4fca1e281b146764646cbdd7d6b1d (patch) | |
| tree | 244f88aebc77a9ca2ef7e69731deb1dfee434ece /powerpc/Asmgenproof.v | |
| parent | e19d179d1f30d5893e5f30dbd33188350656831e (diff) | |
| parent | d194e47a7d494944385ff61c194693f8a67787cb (diff) | |
| download | compcert-kvx-ae2d228c04f4fca1e281b146764646cbdd7d6b1d.tar.gz compcert-kvx-ae2d228c04f4fca1e281b146764646cbdd7d6b1d.zip | |
Merge remote-tracking branch 'origin/master' into towards_3.10
Diffstat (limited to 'powerpc/Asmgenproof.v')
| -rw-r--r-- | powerpc/Asmgenproof.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index e25ae583..b6b5c678 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -294,10 +294,10 @@ Opaque Int.eq. - unfold xorimm64, opimm64. destruct Int64.eq. TailNoLabel. destruct ireg_eq; [apply tail_nolabel_cons; unfold nolabel;auto|]; eapply tail_nolabel_trans; TailNoLabel. - unfold rolm64, andimm64_base, opimm64. - destruct (is_rldl_mask i0 || is_rldr_mask i0 || is_rldl_mask (Int64.shru' i0 i)). TailNoLabel. - apply tail_nolabel_cons; unfold nolabel; auto. + destruct orb. + TailNoLabel. destruct Int64.eq. TailNoLabel. - destruct ireg_eq; [apply tail_nolabel_cons; unfold nolabel;auto|]; eapply tail_nolabel_trans; TailNoLabel. + destruct ireg_eq; TailNoLabel; eapply tail_nolabel_trans; TailNoLabel. - eapply transl_cond_op_label; eauto. - destruct (preg_of r); monadInv H. eapply transl_select_op_label; eauto. eapply transl_fselect_op_label; eauto. Qed. |