branch: elpa/proof-general
commit a894bcc5f915f1c76a2a83c12c12ea3497542426
Author: Pierre Courtieu <[email protected]>
Commit: GitHub <[email protected]>
test: Replace `omega` with `lia` in CI & Test more Coq versions (#650)
* Replace `omega` with `lia` in CI.
* Test more Coq versions.
---
.github/workflows/test.yml | 10 ++++++++++
ci/test_wholefile.v | 8 ++++----
2 files changed, 14 insertions(+), 4 deletions(-)
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 57296e8d49..f239e57504 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -93,6 +93,8 @@ jobs:
- '8.11'
- '8.12'
- '8.13'
+ - '8.14'
+ - '8.15'
ocaml_version:
- minimal
# at most 20 concurrent jobs per free account
@@ -138,6 +140,10 @@ jobs:
- '8.9'
- '8.10'
- '8.11'
+ - '8.12'
+ - '8.13'
+ - '8.14'
+ - '8.15'
ocaml_version:
- minimal
# at most 20 concurrent jobs per free account
@@ -187,6 +193,10 @@ jobs:
- '8.9'
- '8.10'
- '8.11'
+ - '8.12'
+ - '8.13'
+ - '8.14'
+ - '8.15'
ocaml_version:
- minimal
max-parallel: 6
diff --git a/ci/test_wholefile.v b/ci/test_wholefile.v
index 9deee01dd1..261c81703a 100644
--- a/ci/test_wholefile.v
+++ b/ci/test_wholefile.v
@@ -6,7 +6,7 @@ Require Export ArithRing.
Require Export Compare_dec.
Require Export Wf_nat.
Require Export Arith.
-Require Export Omega.
+Require Export Lia.
Theorem minus_minus : forall a b c : nat, a - b - c = a - (b + c).
intros a; elim a; auto.
@@ -37,10 +37,10 @@ Theorem mult_lt : forall a b c : nat, c <> 0 -> a < b -> a
* c < b * c.
intros a b c; elim c.
intros H; elim H; auto.
intros c'; case c'.
-intros; omega.
+intros; lia.
intros c'' Hrec Hneq Hlt;
repeat rewrite <- (fun x : nat => mult_n_Sm x (S c'')).
-auto with *.
+lia.
Qed.
Remark add_sub_square_identity :
@@ -63,7 +63,7 @@ intros x; case x.
intros y; case y; simpl in |- *; auto with *.
intros x' y Hlt; apply lt_trans with (S x' * y).
rewrite (mult_comm (S x') y); apply mult_lt; auto.
-apply mult_lt; omega.
+apply mult_lt; lia.
Qed.
Theorem root_monotonic : forall x y : nat, x * x < y * y -> x < y.
