diff options
Diffstat (limited to 'lib/Decidableplus.v')
| -rw-r--r-- | lib/Decidableplus.v | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/lib/Decidableplus.v b/lib/Decidableplus.v index 66dffb3a..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. *) (* *) (* *********************************************************************) @@ -126,14 +127,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 +147,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. |