Imported Upstream version 8.1~gammaupstream/8.1.gamma

3 files changed, 11 insertions, 10 deletions

diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index dcb7fb49..911de00e 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -11,8 +11,9 @@
  * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
  *              91405 Orsay, France *)
 
-(* $Id: FMapPositive.v 8773 2006-04-29 14:31:32Z letouzey $ *)
+(* $Id: FMapPositive.v 9178 2006-09-26 11:18:22Z barras $ *)
 
+Require Import Bool.
 Require Import ZArith.
 Require Import OrderedType.
 Require Import FMapInterface.
@@ -734,7 +735,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   Proof.
   intros.
   generalize (xelements_complete _ _ _ _ H); clear H; intros.
-  revert H; revert v; revert m; revert q; revert p0.
+  revert p0 q m v H.
   induction p; destruct p0; simpl; intros; eauto; try discriminate.
   Qed.
 
@@ -743,7 +744,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   Proof.
   intros.
   generalize (xelements_complete _ _ _ _ H); clear H; intros.
-  revert H; revert v; revert m; revert q; revert p0.
+  revert p0 q m v H.
   induction p; destruct p0; simpl; intros; eauto; try discriminate.
   Qed.
 
diff --git a/theories/FSets/FSetWeak.v b/theories/FSets/FSetWeak.v
index bfe34cd7..c88a7869 100644
--- a/theories/FSets/FSetWeak.v
+++ b/theories/FSets/FSetWeak.v
@@ -6,11 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id: FSetWeak.v 8819 2006-05-15 09:52:36Z letouzey $ *)
+(* $Id: FSetWeak.v 9278 2006-10-25 13:43:17Z letouzey $ *)
 
 Require Export DecidableType.
 Require Export DecidableTypeEx.
 Require Export FSetWeakInterface.
-Require Export FSetFacts.
-Require Export FSetProperties.
+Require Export FSetWeakFacts.
+Require Export FSetWeakProperties.
 Require Export FSetWeakList.
diff --git a/theories/FSets/OrderedTypeEx.v b/theories/FSets/OrderedTypeEx.v
index 1c5a4054..6fa6a85c 100644
--- a/theories/FSets/OrderedTypeEx.v
+++ b/theories/FSets/OrderedTypeEx.v
@@ -11,7 +11,7 @@
  * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
  *              91405 Orsay, France *)
 
-(* $Id: OrderedTypeEx.v 8836 2006-05-20 21:34:27Z letouzey $ *)
+(* $Id: OrderedTypeEx.v 9066 2006-08-14 10:11:18Z letouzey $ *)
 
 Require Import OrderedType.
 Require Import ZArith.
@@ -66,7 +66,7 @@ Module Nat_as_OT <: UsualOrderedType.
     constructor 1; auto.
     constructor 2; auto.
     intro; constructor 3; auto.
-  Qed.
+  Defined.
 
 End Nat_as_OT.
 
@@ -182,7 +182,7 @@ Module N_as_OT <: UsualOrderedType.
    destruct (Nle x y); auto.
    destruct (x ?= y)%N; simpl; try discriminate.
    intros (H0,_); elim H0; auto.
-  Qed.
+  Defined.
 
 End N_as_OT.
 
@@ -242,7 +242,7 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType.
  apply EQ; unfold eq; auto.
  apply GT; unfold lt; auto.
  apply GT; unfold lt; auto.
- Qed.
+ Defined.
 
 End PairOrderedType.