22 files changed, 0 insertions, 44 deletions
diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v
index 5f6860997..5fbfadd4c 100644
--- a/theories/Sets/Classical_sets.v
+++ b/theories/Sets/Classical_sets.v
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id$ 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 0719365f1..294dbb0cd 100644
--- a/theories/Sets/Constructive_sets.v
+++ b/theories/Sets/Constructive_sets.v
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export Ensembles.
 
 Section Ensembles_facts.
diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v
index 8c69e6877..6d537f59b 100644
--- a/theories/Sets/Cpo.v
+++ b/theories/Sets/Cpo.v
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export Ensembles.
 Require Export Relations_1.
 Require Export Partial_Order.
diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v
index 0fa9c74a8..8843cadd6 100644
--- a/theories/Sets/Ensembles.v
+++ b/theories/Sets/Ensembles.v
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id$ i*)
-
 Section Ensembles.
   Variable U : Type.
 
diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v
index 019c25a55..11ac3b9e4 100644
--- a/theories/Sets/Finite_sets.v
+++ b/theories/Sets/Finite_sets.v
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Ensembles.
 
 Section Ensembles_finis.
diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v
index fdcc4150f..da4a35813 100644
--- a/theories/Sets/Finite_sets_facts.v
+++ b/theories/Sets/Finite_sets_facts.v
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export Finite_sets.
 Require Export Constructive_sets.
 Require Export Classical_Type.
diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v
index 64c341bd3..313a18dcc 100644
--- a/theories/Sets/Image.v
+++ b/theories/Sets/Image.v
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export Finite_sets.
 Require Export Constructive_sets.
 Require Export Classical_Type.
diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v
index b63ec1d47..0ae11b4f6 100644
--- a/theories/Sets/Infinite_sets.v
+++ b/theories/Sets/Infinite_sets.v
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id$ 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 15c1b665e..8fe9928b1 100644
--- a/theories/Sets/Integers.v
+++ b/theories/Sets/Integers.v
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id$ 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 7216ae335..5b7aa24b7 100644
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ 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 4fe8f4f6a..195f454e5 100644
--- a/theories/Sets/Partial_Order.v
+++ b/theories/Sets/Partial_Order.v
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export Ensembles.
 Require Export Relations_1.
 
diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v
index f593031a0..25a121cb3 100644
--- a/theories/Sets/Permut.v
+++ b/theories/Sets/Permut.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (* G. Huet 1-9-95 *)
 
 (** We consider a Set [U], given with a commutative-associative operator [op],
diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v
index c323ca356..9ecb600a5 100644
--- a/theories/Sets/Powerset.v
+++ b/theories/Sets/Powerset.v
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export Ensembles.
 Require Export Relations_1.
 Require Export Relations_1_facts.
diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v
index 36d2150c3..8f881c363 100644
--- a/theories/Sets/Powerset_Classical_facts.v
+++ b/theories/Sets/Powerset_Classical_facts.v
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id$ 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 76f7f1ec8..61f783957 100644
--- a/theories/Sets/Powerset_facts.v
+++ b/theories/Sets/Powerset_facts.v
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id$ 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 85d0cffcc..eb3273959 100644
--- a/theories/Sets/Relations_1.v
+++ b/theories/Sets/Relations_1.v
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id$ i*)
-
 Section Relations_1.
    Variable U : Type.
 
diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v
index fd83b0e0d..484245bc8 100644
--- a/theories/Sets/Relations_1_facts.v
+++ b/theories/Sets/Relations_1_facts.v
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export Relations_1.
 
 Definition Complement (U:Type) (R:Relation U) : Relation U :=
diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v
index 11ac85e84..3b1e7057d 100644
--- a/theories/Sets/Relations_2.v
+++ b/theories/Sets/Relations_2.v
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export Relations_1.
 
 Section Relations_2.
diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v
index 3554901b9..6fd07160f 100644
--- a/theories/Sets/Relations_2_facts.v
+++ b/theories/Sets/Relations_2_facts.v
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export Relations_1.
 Require Export Relations_1_facts.
 Require Export Relations_2.
diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v
index 970db1827..991b38242 100644
--- a/theories/Sets/Relations_3.v
+++ b/theories/Sets/Relations_3.v
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id$ 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 d8bf7dc3c..a2a0f4584 100644
--- a/theories/Sets/Relations_3_facts.v
+++ b/theories/Sets/Relations_3_facts.v
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export Relations_1.
 Require Export Relations_1_facts.
 Require Export Relations_2.
diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v
index 909c79838..41e7f0edf 100644
--- a/theories/Sets/Uniset.v
+++ b/theories/Sets/Uniset.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (** Sets as characteristic functions *)
 
 (* G. Huet 1-9-95 *)