Commit 522285d1 authored by Xavier Leroy's avatar Xavier Leroy
Browse files

Replace `omega` tactic with `lia`, continued

Follow-up to aba0e740
parent 7f152e2f
......@@ -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)).
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment