Remove the svn-specific $Id$ annotations

 - Many of them were broken, some of them after Pierre B's rework
   of mli for ocamldoc, but not only (many bad annotation, many files
   with no svn property about Id, etc)
 - Useless for those of us that work with git-svn (and a fortiori
   in a forthcoming git-only setting)
 - Even in svn, they seem to be of little interest

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7

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 *)