diff options
Diffstat (limited to 'theories/FSets/FMapFullAVL.v')
| -rw-r--r-- | theories/FSets/FMapFullAVL.v | 4 |
1 files changed, 3 insertions, 1 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. |