diff options
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, |