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

9 files changed, 0 insertions, 18 deletions

diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v
index 2c72e30b16..79e817717a 100644
--- a/theories/Structures/DecidableType.v
+++ b/theories/Structures/DecidableType.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
-
 Require Export SetoidList.
 Require Equalities.
 
diff --git a/theories/Structures/DecidableTypeEx.v b/theories/Structures/DecidableTypeEx.v
index 4407ead416..2c02f8ddd1 100644
--- a/theories/Structures/DecidableTypeEx.v
+++ b/theories/Structures/DecidableTypeEx.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
-
 Require Import DecidableType OrderedType OrderedTypeEx.
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v
index 3d4430b9e8..0a6dba982a 100644
--- a/theories/Structures/Equalities.v
+++ b/theories/Structures/Equalities.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
-
 Require Export RelationClasses.
 
 Set Implicit Arguments.
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index 72fbe79680..6b9007fdd3 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
-
 Require Export SetoidList Morphisms OrdersTac.
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/Structures/OrderedTypeAlt.v b/theories/Structures/OrderedTypeAlt.v
index 23ae4c85a3..b054496e9a 100644
--- a/theories/Structures/OrderedTypeAlt.v
+++ b/theories/Structures/OrderedTypeAlt.v
@@ -5,8 +5,6 @@
 (*    //   *      This file is distributed under the terms of the      *)
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
-(* $Id$ *)
-
 Require Import OrderedType.
 
 (** * An alternative (but equivalent) presentation for an Ordered Type
diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v
index a39f336a57..600eabf110 100644
--- a/theories/Structures/OrderedTypeEx.v
+++ b/theories/Structures/OrderedTypeEx.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
-
 Require Import OrderedType.
 Require Import ZArith.
 Require Import Omega.
diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v
index 96daca5cd3..d7bdfbf717 100644
--- a/theories/Structures/Orders.v
+++ b/theories/Structures/Orders.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
-
 Require Export Relations Morphisms Setoid Equalities.
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/Structures/OrdersAlt.v b/theories/Structures/OrdersAlt.v
index d86b02a15e..85e7fb176e 100644
--- a/theories/Structures/OrdersAlt.v
+++ b/theories/Structures/OrdersAlt.v
@@ -11,8 +11,6 @@
  * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
  *              91405 Orsay, France *)
 
-(* $Id$ *)
-
 Require Import OrderedType Orders.
 Set Implicit Arguments.
 
diff --git a/theories/Structures/OrdersEx.v b/theories/Structures/OrdersEx.v
index b0702f6818..f8a08bf4e9 100644
--- a/theories/Structures/OrdersEx.v
+++ b/theories/Structures/OrdersEx.v
@@ -11,8 +11,6 @@
  * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
  *              91405 Orsay, France *)
 
-(* $Id$ *)
-
 Require Import Orders NPeano POrderedType NArith
  ZArith RelationPairs EqualitiesFacts.