diff options
Diffstat (limited to 'theories/FSets')
| -rw-r--r-- | theories/FSets/FMapFullAVL.v | 4 | ||||
| -rw-r--r-- | theories/FSets/FSetFullAVL.v | 4 |
2 files changed, 6 insertions, 2 deletions
diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v index ae3bdb8162..3ebb0c1afb 100644 --- a/theories/FSets/FMapFullAVL.v +++ b/theories/FSets/FMapFullAVL.v @@ -28,7 +28,7 @@ *) -Require Import Recdef FMapInterface FMapList ZArith Int FMapAVL. +Require Import Recdef FMapInterface FMapList ZArith Int FMapAVL ROmega. Set Implicit Arguments. Unset Strict Implicit. @@ -40,6 +40,8 @@ Import Raw.Proofs. Open Local Scope pair_scope. Open Local Scope Int_scope. +Ltac omega_max := i2z_refl; romega with Z. + Section Elt. Variable elt : Type. Implicit Types m r : t elt. 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, |