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

3 files changed, 16 insertions, 15 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,
diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v
index 562000d8fd..24d2696c59 100644
--- a/theories/ZArith/Int.v
+++ b/theories/ZArith/Int.v
@@ -22,7 +22,6 @@
 *)
 
 Require Import ZArith. 
-Require Import ROmega. 
 Delimit Scope Int_scope with I.
 
 
@@ -135,23 +134,23 @@ Module MoreInt (I:Int).
     | |- (eq (A:=int) ?a ?b) => apply (i2z_eq a b); i2z_gen
     | H : (eq (A:=int) ?a ?b) |- _ => 
        generalize (f_equal i2z H); clear H; i2z_gen
-    | H : (eq (A:=Z) ?a ?b) |- _ => generalize H; clear H; i2z_gen
-    | H : (Zlt ?a ?b) |- _ => generalize H; clear H; i2z_gen
-    | H : (Zle ?a ?b) |- _ => generalize H; clear H; i2z_gen
-    | H : (Zgt ?a ?b) |- _ => generalize H; clear H; i2z_gen
-    | H : (Zge ?a ?b) |- _ => generalize H; clear H; i2z_gen
+    | H : (eq (A:=Z) ?a ?b) |- _ => revert H; i2z_gen
+    | H : (Zlt ?a ?b) |- _ => revert H; i2z_gen
+    | H : (Zle ?a ?b) |- _ => revert H; i2z_gen
+    | H : (Zgt ?a ?b) |- _ => revert H; i2z_gen
+    | H : (Zge ?a ?b) |- _ => revert H; i2z_gen
     | H : _ -> ?X |- _ => 
       (* A [Set] or [Type] part cannot be dealt with easily
          using the [ExprP] datatype. So we forget it, leaving 
          a goal that can be weaker than the original. *)
       match type of X with 
        | Type => clear H; i2z_gen
-       | Prop => generalize H; clear H; i2z_gen
+       | Prop => revert H; i2z_gen
       end
-    | H : _ <-> _ |- _ => generalize H; clear H; i2z_gen
-    | H : _ /\ _ |- _ => generalize H; clear H; i2z_gen
-    | H : _ \/ _ |- _ => generalize H; clear H; i2z_gen
-    | H : ~ _ |- _ => generalize H; clear H; i2z_gen
+    | H : _ <-> _ |- _ => revert H; i2z_gen
+    | H : _ /\ _ |- _ => revert H; i2z_gen
+    | H : _ \/ _ |- _ => revert H; i2z_gen
+    | H : ~ _ |- _ => revert H; i2z_gen
     | _ => idtac
    end.
 
@@ -358,8 +357,6 @@ Module MoreInt (I:Int).
 
   (* i2z_refl can be replaced below by (simpl in *; i2z). 
      The reflexive version improves compilation of AVL files by about 15%  *)
-  
-  Ltac omega_max := i2z_refl; romega with Z.
 
 End MoreInt.