From abdf4058321e3767421cd0c30d8f4fc63e0518e3 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Thu, 10 Oct 2019 12:14:55 +0000
Subject: FSets: do not use “omega”

---
 theories/FSets/FMapAVL.v      | 3 ++-
 theories/FSets/FMapFullAVL.v  | 2 +-
 theories/FSets/FMapPositive.v | 4 ++--
 3 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 7c69350db4..ea4062d9fe 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -1363,7 +1363,8 @@ Lemma elements_aux_cardinal :
 Proof.
  simple induction m; simpl; intuition.
  rewrite <- H; simpl.
- rewrite <- H0; omega.
+ rewrite <- H0, Nat.add_succ_r, (Nat.add_comm (cardinal t)), Nat.add_assoc.
+ reflexivity.
 Qed.
 
 Lemma elements_cardinal : forall (m:t elt), cardinal m = length (elements m).
diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v
index 0ef356b582..fa553d9fce 100644
--- a/theories/FSets/FMapFullAVL.v
+++ b/theories/FSets/FMapFullAVL.v
@@ -68,7 +68,7 @@ Hint Constructors avl : core.
 Lemma height_non_negative : forall (s : t elt), avl s ->
  height s >= 0.
 Proof.
- induction s; simpl; intros; auto with zarith.
+ induction s; simpl; intros. now apply Z.le_ge.
  inv avl; intuition; omega_max.
 Qed.
 
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index e5133f66b2..342a51b39b 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -476,8 +476,8 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
    unfold elements.
    intros m; set (p:=1); clearbody p; revert m p.
    induction m; simpl; auto; intros.
-   rewrite (IHm1 (append p 2)), (IHm2 (append p 3)); auto.
-   destruct o; rewrite app_length; simpl; omega.
+   rewrite (IHm1 (append p 2)), (IHm2 (append p 3)).
+   destruct o; rewrite app_length; simpl; auto.
   Qed.
 
   End CompcertSpec.
-- 
cgit v1.2.3