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`. --- lib/Decidableplus.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'lib/Decidableplus.v') diff --git a/lib/Decidableplus.v b/lib/Decidableplus.v index 66dffb3a..73f080b6 100644 --- a/lib/Decidableplus.v +++ b/lib/Decidableplus.v @@ -126,14 +126,14 @@ Program Instance Decidable_ge_Z : forall (x y: Z), Decidable (x >= y) := { Decidable_witness := Z.geb x y }. Next Obligation. - rewrite Z.geb_le. intuition omega. + rewrite Z.geb_le. intuition lia. Qed. Program Instance Decidable_gt_Z : forall (x y: Z), Decidable (x > y) := { Decidable_witness := Z.gtb x y }. Next Obligation. - rewrite Z.gtb_lt. intuition omega. + rewrite Z.gtb_lt. intuition lia. Qed. Program Instance Decidable_divides : forall (x y: Z), Decidable (x | y) := { @@ -146,7 +146,7 @@ Next Obligation. destruct (Z.eq_dec x 0). subst x. rewrite Z.mul_0_r in EQ. subst y. reflexivity. assert (k = y / x). - { apply Zdiv_unique_full with 0. red; omega. rewrite EQ; ring. } + { apply Zdiv_unique_full with 0. red; lia. rewrite EQ; ring. } congruence. Qed. -- cgit From 04f499c632a76e460560fc9ec4e14d8216e7fc18 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 4 May 2021 10:46:17 +0200 Subject: Use the LGPL instead of the GPL for dual-licensed files The GPL makes sense for whole applications, but the dual-licensed Coq and OCaml files are more like libraries to be combined with other code, so the LGPL is more appropriate. --- lib/Decidableplus.v | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'lib/Decidableplus.v') diff --git a/lib/Decidableplus.v b/lib/Decidableplus.v index 73f080b6..69ba4723 100644 --- a/lib/Decidableplus.v +++ b/lib/Decidableplus.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) -- cgit