diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-03-28 18:16:22 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-03-28 18:16:22 +0000 |
| commit | 29e7f5e8aba98c8d9dbdb8ca64fd8aed5b705d38 (patch) | |
| tree | c0e30892b89db7cdec606815bf027c2d41ad59dc /theories/FSets | |
| 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')
| -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 ae3bdb816..3ebb0c1af 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 64d5eb8af..81ed9a572 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, |