diff options
Diffstat (limited to 'powerpc/SelectOpproof.v')
| -rw-r--r-- | powerpc/SelectOpproof.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index ed81c83f..edc935d4 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -809,7 +809,7 @@ Qed. Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8). Proof. red; intros. unfold cast8unsigned. - rewrite Val.zero_ext_and. apply eval_andimm; auto. omega. + rewrite Val.zero_ext_and. apply eval_andimm; auto. lia. Qed. Theorem eval_cast16signed: unary_constructor_sound cast16signed (Val.sign_ext 16). @@ -822,7 +822,7 @@ Qed. Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ext 16). Proof. red; intros. unfold cast16unsigned. - rewrite Val.zero_ext_and. apply eval_andimm; auto. omega. + rewrite Val.zero_ext_and. apply eval_andimm; auto. lia. Qed. Theorem eval_singleoffloat: unary_constructor_sound singleoffloat Val.singleoffloat. @@ -860,7 +860,7 @@ Proof. simpl; rewrite Heqo; simpl; eauto. constructor. simpl. unfold Int64.loword. rewrite Int64.unsigned_repr, Int.repr_unsigned. auto. assert (Int.modulus < Int64.max_unsigned) by (compute; auto). - generalize (Int.unsigned_range n). omega. + generalize (Int.unsigned_range n). lia. - set (im := Int.repr Int.half_modulus). set (fm := Float.of_intu im). assert (eval_expr ge sp e m (Vfloat fm :: Vfloat f :: le) (Eletvar (S O)) (Vfloat f)). |