diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-01-13 14:51:36 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-01-13 14:51:36 +0100 |
| commit | 522285d1163523b02a1972b99d71c08552cd9c7b (patch) | |
| tree | a1d9b43928276e90c8223a9736253d19f52f2bca /powerpc | |
| parent | 7f152e2f27d82f0d502ee919e1576edefcd44cf5 (diff) | |
| download | compcert-kvx-522285d1163523b02a1972b99d71c08552cd9c7b.tar.gz compcert-kvx-522285d1163523b02a1972b99d71c08552cd9c7b.zip | |
Replace `omega` tactic with `lia`, continued
Follow-up to aba0e740f
Diffstat (limited to 'powerpc')
| -rw-r--r-- | powerpc/SelectOpproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 73fadc46..adac6c34 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -856,7 +856,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)). |