From aba0e740f25ffa5c338dfa76cab71144802cebc2 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 21 Jun 2020 18:22:00 +0200 Subject: Replace `omega` tactic with `lia` Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`. --- arm/Op.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'arm/Op.v') diff --git a/arm/Op.v b/arm/Op.v index cc90e043..4739ef2e 100644 --- a/arm/Op.v +++ b/arm/Op.v @@ -527,10 +527,10 @@ End SOUNDNESS. Program Definition mk_shift_amount (n: int) : shift_amount := {| s_amount := Int.modu n Int.iwordsize; s_range := _ |}. Next Obligation. - assert (0 <= Z.modulo (Int.unsigned n) 32 < 32). apply Z_mod_lt. omega. + assert (0 <= Z.modulo (Int.unsigned n) 32 < 32). apply Z_mod_lt. lia. unfold Int.ltu, Int.modu. change (Int.unsigned Int.iwordsize) with 32. - rewrite Int.unsigned_repr. apply zlt_true. omega. - assert (32 < Int.max_unsigned). compute; auto. omega. + rewrite Int.unsigned_repr. apply zlt_true. lia. + assert (32 < Int.max_unsigned). compute; auto. lia. Qed. Lemma mk_shift_amount_eq: -- cgit