From 791ea687b5bbcca4cfc3dc53a57a3ff10037229e Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Mon, 28 Oct 2019 12:51:30 +0000
Subject: PermutEq: use “lia” rather than “omega”

---
 theories/Sorting/PermutEq.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Sorting/PermutEq.v b/theories/Sorting/PermutEq.v
index 8e8f05dabc..4feeb9bfff 100644
--- a/theories/Sorting/PermutEq.v
+++ b/theories/Sorting/PermutEq.v
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-Require Import Relations Setoid SetoidList List Multiset PermutSetoid Permutation Omega.
+Require Import Relations Setoid SetoidList List Multiset PermutSetoid Permutation Lia.
 
 Set Implicit Arguments.
 
@@ -85,7 +85,7 @@ Section Perm.
     rewrite multiplicity_NoDup in H, H0.
     generalize (H a) (H0 a) (H1 a); clear H H0 H1.
     do 2 rewrite multiplicity_In.
-    destruct 3; omega.
+    destruct 3; lia.
   Qed.
 
   (** Permutation is compatible with In. *)
-- 
cgit v1.2.3