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/Init/Datatypes.v b/theories/Init/Datatypes.v
index 092fce996f..782ff6ca95 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Set Implicit Arguments.
 
 Require Import Notations.
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 4fca1d1dbb..14832e0b72 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Set Implicit Arguments.
 
 Require Import Notations.
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index 1333f3545e..ff6a18e147 100644
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (** This module defines type constructors for types in [Type]
     ([Datatypes.v] and [Logic.v] defined them for types in [Set]) *)
 
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 0c628298dc..9bf921b225 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (** These are the notations whose level and associativity are imposed by Coq *)
 
 (** Notations for propositional connectives *)
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 8779f2b452..045210d0ae 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (** The type [nat] of Peano natural numbers (built from [O] and [S])
     is defined in [Datatypes.v] *)
 
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 45b949716c..c8d809fd48 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export Notations.
 Require Export Logic.
 Require Export Datatypes.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 7141f26cb5..6ff8202995 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (** Basic specifications : sets that may contain logical information *)
 
 Set Implicit Arguments.
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 6ccf8a0228..66f90e18f1 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Notations.
 Require Import Logic.
 Require Import Specif.
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index 3209860f34..0a1a0f9b8c 100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (** * This module proves the validity of
     - well-founded recursion (also known as course of values)
     - well-founded induction