6 files changed, 16 insertions, 16 deletions
diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v
index 47554ac4..ae2143c8 100644
--- a/theories/Sets/Infinite_sets.v
+++ b/theories/Sets/Infinite_sets.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Infinite_sets.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Infinite_sets.v 10637 2008-03-07 23:52:56Z letouzey $ i*)
 
 Require Export Finite_sets.
 Require Export Constructive_sets.
@@ -162,7 +162,7 @@ Section Infinite_sets.
     generalize (H'3 x).
     intro H'4; lapply H'4; [ intro H'8; try exact H'8; clear H'4 | clear H'4 ];
       auto with sets.
-    specialize  5Im_inv with (U := U) (V := V) (X := A) (f := f) (y := x);
+    specialize Im_inv with (U := U) (V := V) (X := A) (f := f) (y := x);
       intro H'11; lapply H'11; [ intro H'13; elim H'11; clear H'11 | clear H'11 ];
 	auto with sets.
     intros x1 H'4; try assumption.
diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v
index c969ad9c..1786edf1 100644
--- a/theories/Sets/Integers.v
+++ b/theories/Sets/Integers.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Integers.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Integers.v 10637 2008-03-07 23:52:56Z letouzey $ i*)
 
 Require Export Finite_sets.
 Require Export Constructive_sets.
@@ -87,7 +87,7 @@ Section Integers_sect.
     apply Totally_ordered_definition.
     simpl in |- *.
     intros H' x y H'0.
-    specialize  2le_or_lt with (n := x) (m := y); intro H'2; elim H'2.
+    elim le_or_lt with (n := x) (m := y).
     intro H'1; left; auto with sets arith.
     intro H'1; right.
     cut (y <= x); auto with sets arith.
@@ -142,8 +142,8 @@ Section Integers_sect.
     elim H'0; intros H'1 H'2.
     cut (In nat Integers (S x)).
     intro H'3.
-    specialize  1H'2 with (y := S x); intro H'4; lapply H'4;
-      [ intro H'5; clear H'4 | try assumption; clear H'4 ].
+    specialize H'2 with (y := S x); lapply H'2;
+      [ intro H'5; clear H'2 | try assumption; clear H'2 ].
     simpl in H'5.
     absurd (S x <= x); auto with arith.
     apply triv_nat.
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v
index 7084a82d..d2bff488 100644
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Multiset.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Multiset.v 10616 2008-03-04 17:33:35Z letouzey $ i*)
 
 (* G. Huet 1-9-95 *)
 
@@ -16,11 +16,11 @@ Set Implicit Arguments.
 
 Section multiset_defs.
 
-  Variable A : Set.
+  Variable A : Type.
   Variable eqA : A -> A -> Prop.
   Hypothesis Aeq_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
 
-  Inductive multiset : Set :=
+  Inductive multiset : Type :=
     Bag : (A -> nat) -> multiset.
   
   Definition EmptyBag := Bag (fun a:A => 0).
diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v
index a7c3db3a..4380f10c 100644
--- a/theories/Sets/Permut.v
+++ b/theories/Sets/Permut.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Permut.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Permut.v 10616 2008-03-04 17:33:35Z letouzey $ i*)
 
 (* G. Huet 1-9-95 *)
 
@@ -15,7 +15,7 @@
 
 Section Axiomatisation.
 
-  Variable U : Set.
+  Variable U : Type.
   Variable op : U -> U -> U.
   Variable cong : U -> U -> Prop.
 
diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v
index 47857705..34c49409 100644
--- a/theories/Sets/Powerset_Classical_facts.v
+++ b/theories/Sets/Powerset_Classical_facts.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Powerset_Classical_facts.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Powerset_Classical_facts.v 10855 2008-04-27 11:16:15Z msozeau $ i*)
 
 Require Export Ensembles.
 Require Export Constructive_sets.
diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v
index 3291f3ee..2374c2bf 100644
--- a/theories/Sets/Relations_2_facts.v
+++ b/theories/Sets/Relations_2_facts.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Relations_2_facts.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Relations_2_facts.v 10637 2008-03-07 23:52:56Z letouzey $ i*)
 
 Require Export Relations_1.
 Require Export Relations_1_facts.
@@ -140,10 +140,10 @@ intros U R H' x b H'0; elim H'0.
 intros x0 a H'1; exists a; auto with sets.
 intros x0 y z H'1 H'2 H'3 a H'4.
 red in H'.
-specialize  3H' with (x := x0) (a := a) (b := y); intro H'7; lapply H'7;
+specialize H' with (x := x0) (a := a) (b := y); lapply H'; 
  [ intro H'8; lapply H'8;
-    [ intro H'9; try exact H'9; clear H'8 H'7 | clear H'8 H'7 ]
- | clear H'7 ]; auto with sets.
+    [ intro H'9; try exact H'9; clear H'8 H' | clear H'8 H' ]
+ | clear H' ]; auto with sets.
 elim H'9.
 intros t H'5; elim H'5; intros H'6 H'7; try exact H'6; clear H'5.
 elim (H'3 t); auto with sets.