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

8 files changed, 0 insertions, 16 deletions

diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index 0a35ef45e..75c51a8dd 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -12,8 +12,6 @@
    Institution: LRI, CNRS UMR 8623 - University Paris Sud
 *)
 
-(* $Id$ *)
-
 (** Export notations. *)
 
 Require Export Coq.Classes.Equivalence.
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index d0f243474..d62bd0674 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -12,8 +12,6 @@
    Institution: LRI, CNRS UMR 8623 - University Paris Sud
 *)
 
-(* $Id$ *)
-
 Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
 
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index f6e51018a..df288add4 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -13,8 +13,6 @@
    Institution: LRI, CNRS UMR 8623 - University Paris Sud
 *)
 
-(* $Id$ *)
-
 (** Hints for the proof search: these combinators should be considered rigid. *)
 
 Require Import Coq.Program.Basics.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 4b827c244..2421c90d0 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -13,8 +13,6 @@
    Institution: LRI, CNRS UMR 8623 - University Paris Sud
 *)
 
-(* $Id$ *)
-
 Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
 Require Import Coq.Relations.Relation_Definitions.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index a8193ef3c..4c39964a9 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -15,8 +15,6 @@
    Institution: LRI, CNRS UMR 8623 - University Paris Sud
 *)
 
-(* $Id$ *)
-
 Require Export Coq.Classes.Init.
 Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index c41c57698..36fe2b9a6 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -12,8 +12,6 @@
    Institution: LRI, CNRS UMR 8623 - University Paris Sud
 *)
 
-(* $Id$ *)
-
 Set Implicit Arguments.
 Unset Strict Implicit.
 
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 33b4350f8..ab2131185 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -13,8 +13,6 @@
    Institution: LRI, CNRS UMR 8623 - University Paris Sud
 *)
 
-(* $Id$ *)
-
 Set Implicit Arguments.
 Unset Strict Implicit.
 
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 669be8b0f..dbdff45f3 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -12,8 +12,6 @@
    Institution: LRI, CNRS UMR 8623 - University Paris Sud
 *)
 
-(* $Id$ *)
-
 Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
 Require Export Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions.
 Require Import Coq.Classes.Equivalence Coq.Program.Basics.