Imported Upstream version 8.4~betaupstream/8.4_beta

22 files changed, 35 insertions, 79 deletions

diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v
index 701d9f8a..f93631c7 100644
--- a/theories/Sets/Classical_sets.v
+++ b/theories/Sets/Classical_sets.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Classical_sets.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Export Ensembles.
 Require Export Constructive_sets.
 Require Export Classical_Type.
diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v
index d3900446..e6dd8381 100644
--- a/theories/Sets/Constructive_sets.v
+++ b/theories/Sets/Constructive_sets.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Constructive_sets.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Export Ensembles.
 
 Section Ensembles_facts.
diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v
index c7b496cb..d612e71e 100644
--- a/theories/Sets/Cpo.v
+++ b/theories/Sets/Cpo.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Cpo.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Export Ensembles.
 Require Export Relations_1.
 Require Export Partial_Order.
@@ -107,4 +105,4 @@ Section Specific_orders.
     {PO_of_chain : PO U;
     Chain_cond : Totally_ordered U PO_of_chain (Carrier_of U PO_of_chain)}.
 
-End Specific_orders.
\ No newline at end of file
+End Specific_orders.
diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v
index 6c80ad40..58b979dd 100644
--- a/theories/Sets/Ensembles.v
+++ b/theories/Sets/Ensembles.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Ensembles.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Section Ensembles.
   Variable U : Type.
 
diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v
index 09a0a94d..f0843675 100644
--- a/theories/Sets/Finite_sets.v
+++ b/theories/Sets/Finite_sets.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Finite_sets.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Import Ensembles.
 
 Section Ensembles_finis.
diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v
index a9fe8ffe..350cd783 100644
--- a/theories/Sets/Finite_sets_facts.v
+++ b/theories/Sets/Finite_sets_facts.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Finite_sets_facts.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Export Finite_sets.
 Require Export Constructive_sets.
 Require Export Classical_Type.
@@ -175,14 +173,14 @@ Section Finite_sets_facts.
     clear H'2 c2 Y.
     intros X0 c2 H'2 H'3 x0 H'4 H'5.
     elim (classic (In U X0 x)).
-    intro H'6; apply f_equal with nat.
+    intro H'6; apply f_equal.
     apply H'0 with (Y := Subtract U (Add U X0 x0) x).
     elimtype (pred (S c2) = c2); auto with sets.
     apply card_soustr_1; auto with sets.
     rewrite <- H'5.
     apply Sub_Add_new; auto with sets.
     elim (classic (x = x0)).
-    intros H'6 H'7; apply f_equal with nat.
+    intros H'6 H'7; apply f_equal.
     apply H'0 with (Y := X0); auto with sets.
     apply Simplify_add with (x := x); auto with sets.
     pattern x at 2 in |- *; rewrite H'6; auto with sets.
diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v
index e5eae17e..24facb6f 100644
--- a/theories/Sets/Image.v
+++ b/theories/Sets/Image.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Image.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Export Finite_sets.
 Require Export Constructive_sets.
 Require Export Classical_Type.
@@ -202,4 +200,4 @@ Section Image.
 
 End Image.
 
-Hint Resolve Im_def image_empty finite_image: sets v62.
\ No newline at end of file
+Hint Resolve Im_def image_empty finite_image: sets v62.
diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v
index afb9e0e1..a21fe880 100644
--- a/theories/Sets/Infinite_sets.v
+++ b/theories/Sets/Infinite_sets.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Infinite_sets.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Export Finite_sets.
 Require Export Constructive_sets.
 Require Export Classical_Type.
diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v
index 5d073a0c..2c94a2e1 100644
--- a/theories/Sets/Integers.v
+++ b/theories/Sets/Integers.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Integers.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Export Finite_sets.
 Require Export Constructive_sets.
 Require Export Classical_Type.
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v
index 6187c08b..5f21335f 100644
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Multiset.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (* G. Huet 1-9-95 *)
 
 Require Import Permut Setoid.
diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v
index e819cafa..a319b983 100644
--- a/theories/Sets/Partial_Order.v
+++ b/theories/Sets/Partial_Order.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Partial_Order.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Export Ensembles.
 Require Export Relations_1.
 
@@ -99,4 +97,4 @@ Section Partial_order_facts.
     apply Strict_Rel_Transitive_with_Rel with (y := y);
       [ intuition | unfold Strict_Rel_of in H', H'0; intuition ].
   Qed.
-End Partial_order_facts.
\ No newline at end of file
+End Partial_order_facts.
diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v
index 8699eed3..e28a1264 100644
--- a/theories/Sets/Permut.v
+++ b/theories/Sets/Permut.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Permut.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (* G. Huet 1-9-95 *)
 
 (** We consider a Set [U], given with a commutative-associative operator [op],
@@ -86,4 +84,4 @@ Section Axiomatisation.
     apply cong_left; apply perm_left.
   Qed.
 
-End Axiomatisation.
\ No newline at end of file
+End Axiomatisation.
diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v
index 372473d6..f8b24e74 100644
--- a/theories/Sets/Powerset.v
+++ b/theories/Sets/Powerset.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Powerset.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Export Ensembles.
 Require Export Relations_1.
 Require Export Relations_1_facts.
@@ -187,4 +185,4 @@ Hint Resolve Union_increases_r: sets v62.
 Hint Resolve Intersection_decreases_l: sets v62.
 Hint Resolve Intersection_decreases_r: sets v62.
 Hint Resolve Empty_set_is_Bottom: sets v62.
-Hint Resolve Strict_inclusion_is_transitive: sets v62.
\ No newline at end of file
+Hint Resolve Strict_inclusion_is_transitive: sets v62.
diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v
index 66c0c0bb..09fc2094 100644
--- a/theories/Sets/Powerset_Classical_facts.v
+++ b/theories/Sets/Powerset_Classical_facts.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Powerset_Classical_facts.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Export Ensembles.
 Require Export Constructive_sets.
 Require Export Relations_1.
diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v
index 09edd08a..f756f985 100644
--- a/theories/Sets/Powerset_facts.v
+++ b/theories/Sets/Powerset_facts.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Powerset_facts.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Export Ensembles.
 Require Export Constructive_sets.
 Require Export Relations_1.
diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v
index 2818b370..a7fbb53d 100644
--- a/theories/Sets/Relations_1.v
+++ b/theories/Sets/Relations_1.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Relations_1.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Section Relations_1.
    Variable U : Type.
 
@@ -64,4 +62,4 @@ End Relations_1.
 Hint Unfold Reflexive Transitive Antisymmetric Symmetric contains
   same_relation: sets v62.
 Hint Resolve Definition_of_preorder Definition_of_order
-  Definition_of_equivalence Definition_of_PER: sets v62.
\ No newline at end of file
+  Definition_of_equivalence Definition_of_PER: sets v62.
diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v
index f002e926..0c8329dd 100644
--- a/theories/Sets/Relations_1_facts.v
+++ b/theories/Sets/Relations_1_facts.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Relations_1_facts.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Export Relations_1.
 
 Definition Complement (U:Type) (R:Relation U) : Relation U :=
@@ -109,4 +107,4 @@ intros U R R' H' H'0; red in |- *.
 elim H'.
 intros H'1 H'2 x y z H'3 H'4; apply H'2.
 apply H'0 with y; auto with sets.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v
index 710bff2b..e7a69c99 100644
--- a/theories/Sets/Relations_2.v
+++ b/theories/Sets/Relations_2.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Relations_2.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Export Relations_1.
 
 Section Relations_2.
@@ -53,4 +51,4 @@ End Relations_2.
 Hint Resolve Rstar_0: sets v62.
 Hint Resolve Rstar1_0: sets v62.
 Hint Resolve Rstar1_1: sets v62.
-Hint Resolve Rplus_0: sets v62.
\ No newline at end of file
+Hint Resolve Rplus_0: sets v62.
diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v
index 5ccdcb11..89b98c1f 100644
--- a/theories/Sets/Relations_2_facts.v
+++ b/theories/Sets/Relations_2_facts.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Relations_2_facts.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Export Relations_1.
 Require Export Relations_1_facts.
 Require Export Relations_2.
@@ -150,4 +148,4 @@ elim (H'3 t); auto with sets.
 intros z1 H'5; elim H'5; intros H'8 H'10; try exact H'8; clear H'5.
 exists z1; split; [ idtac | assumption ].
 apply Rstar_n with t; auto with sets.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v
index 1f96a75a..51092f7a 100644
--- a/theories/Sets/Relations_3.v
+++ b/theories/Sets/Relations_3.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Relations_3.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Export Relations_1.
 Require Export Relations_2.
 
diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v
index 3a69a231..8ac6e7fb 100644
--- a/theories/Sets/Relations_3_facts.v
+++ b/theories/Sets/Relations_3_facts.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Relations_3_facts.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Export Relations_1.
 Require Export Relations_1_facts.
 Require Export Relations_2.
@@ -168,4 +166,4 @@ generalize (H'2 v); intro h; lapply h;
 red in |- *; (exists z1; split); auto with sets.
 apply T with y1; auto with sets.
 apply T with t; auto with sets.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v
index 48789f9a..bf1aaf8d 100644
--- a/theories/Sets/Uniset.v
+++ b/theories/Sets/Uniset.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Uniset.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (** Sets as characteristic functions *)
 
 (* G. Huet 1-9-95 *)
@@ -212,4 +210,4 @@ i*)
 
 End defs.
 
-Unset Implicit Arguments.
\ No newline at end of file
+Unset Implicit Arguments.