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 2c72e30b1..79e817717 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 4407ead41..2c02f8ddd 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 3d4430b9e..0a6dba982 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 72fbe7968..6b9007fdd 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 23ae4c85a..b054496e9 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 a39f336a5..600eabf11 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 96daca5cd..d7bdfbf71 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 d86b02a15..85e7fb176 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 b0702f681..f8a08bf4e 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.