From 29e7f5e8aba98c8d9dbdb8ca64fd8aed5b705d38 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Sat, 28 Mar 2009 18:16:22 +0000
Subject: ZArith/Int: no need to load romega here (but rather in FullAVL)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12027 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/FSets/FSetFullAVL.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'theories/FSets/FSetFullAVL.v')

diff --git a/theories/FSets/FSetFullAVL.v b/theories/FSets/FSetFullAVL.v
index 64d5eb8af6..81ed9a5726 100644
--- a/theories/FSets/FSetFullAVL.v
+++ b/theories/FSets/FSetFullAVL.v
@@ -30,7 +30,7 @@
    similar to the one of [FSetAVL], but richer.
 *)
 
-Require Import Recdef FSetInterface FSetList ZArith Int FSetAVL.
+Require Import Recdef FSetInterface FSetList ZArith Int FSetAVL ROmega.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -42,6 +42,8 @@ Module Import II := MoreInt I.
 Open Local Scope pair_scope.
 Open Local Scope Int_scope.
 
+Ltac omega_max := i2z_refl; romega with Z.
+
 (** * AVL trees *)
 
 (** [avl s] : [s] is a properly balanced AVL tree,
-- 
cgit v1.2.3