From 522285d1163523b02a1972b99d71c08552cd9c7b Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 13 Jan 2021 14:51:36 +0100 Subject: Replace `omega` tactic with `lia`, continued Follow-up to aba0e740f --- powerpc/SelectOpproof.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'powerpc') 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)). -- cgit