Replace the use of omega with lia

coq-community · May 12, 2021 · 58f3fa4 · 58f3fa4
1 parent 450fc53
commit 58f3fa4
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 3 deletions.
diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
@@ -17,6 +17,7 @@ jobs:
     strategy:
       matrix:
         image:
+          - 'mathcomp/mathcomp:1.12.0-coq-dev'
           - 'mathcomp/mathcomp:1.12.0-coq-8.13'
           - 'mathcomp/mathcomp:1.12.0-coq-8.12'
           - 'mathcomp/mathcomp:1.12.0-coq-8.11'

diff --git a/meta.yml b/meta.yml
@@ -83,6 +83,8 @@ dependencies:
     [MathComp](https://math-comp.github.io) 1.11.0 or later
 
 tested_coq_opam_versions:
+- version: '1.12.0-coq-dev'
+  repo: 'mathcomp/mathcomp'
 - version: '1.12.0-coq-8.13'
   repo: 'mathcomp/mathcomp'
 - version: '1.12.0-coq-8.12'

diff --git a/refinements/binnat.v b/refinements/binnat.v
@@ -1,6 +1,6 @@
 (** This file is part of CoqEAL, the Coq Effective Algebra Library.
 (c) Copyright INRIA and University of Gothenburg, see LICENSE *)
-Require Import ZArith.
+Require Import ZArith Lia.
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq zmodp.
 From mathcomp Require Import path choice fintype tuple finset ssralg ssrnum bigop ssrint.
@@ -405,13 +405,13 @@ Qed.
 Lemma Nat2Pos_xI m : ((Pos.of_nat m.+1)~1)%positive = Pos.of_nat ((m.+1).*2.+1).
 Proof.
 rewrite -muln2 [RHS]Nat2Pos.inj_succ // Nat2Pos.inj_mul //.
-simpl (Pos.of_nat 2); zify; omega.
+simpl (Pos.of_nat 2); lia.
 Qed.
 
 Lemma Nat2Pos_xO m : ((Pos.of_nat m.+1)~0)%positive = Pos.of_nat ((m.+1).*2).
 Proof.
 rewrite -muln2 Nat2Pos.inj_mul //.
-simpl (Pos.of_nat 2); zify; omega.
+simpl (Pos.of_nat 2); lia.
 Qed.
 
 Lemma pos_of_natE m n : pos_of_nat m n = Pos.of_nat (maxn 1 (m.*2.+1 - n)).