diff options
| author | letouzey | 2009-03-28 18:16:22 +0000 |
|---|---|---|
| committer | letouzey | 2009-03-28 18:16:22 +0000 |
| commit | 29e7f5e8aba98c8d9dbdb8ca64fd8aed5b705d38 (patch) | |
| tree | c0e30892b89db7cdec606815bf027c2d41ad59dc /theories/FSets/FSetFullAVL.v | |
| parent | 7c3f7a3c4ee9b75ee3e244fd425cb573ae72403c (diff) | |
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
Diffstat (limited to 'theories/FSets/FSetFullAVL.v')
| -rw-r--r-- | theories/FSets/FSetFullAVL.v | 4 |
1 files changed, 3 insertions, 1 deletions
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, |