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

7 files changed, 0 insertions, 13 deletions

diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 66ab6f1c8b..a1ea2ebc8c 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (** The type [bool] is defined in the prelude as
     [Inductive bool : Set := true : bool | false : bool] *)
 
diff --git a/theories/Bool/BoolEq.v b/theories/Bool/BoolEq.v
index 625cbd194d..9a2e738ebf 100644
--- a/theories/Bool/BoolEq.v
+++ b/theories/Bool/BoolEq.v
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
 (* Cuihtlauac Alvarado - octobre 2000 *)
 
 (** Properties of a boolean equality   *)
diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v
index d9da086721..b41d65c39c 100644
--- a/theories/Bool/Bvector.v
+++ b/theories/Bool/Bvector.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (** Bit vectors. Contribution by Jean Duprat (ENS Lyon). *)
 
 Require Export Bool Sumbool.
diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v
index 90f7ee662f..799438d89f 100644
--- a/theories/Bool/DecBool.v
+++ b/theories/Bool/DecBool.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Set Implicit Arguments.
 
 Definition ifdec (A B:Prop) (C:Type) (H:{A} + {B}) (x y:C) : C :=
diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v
index c2b5ed7932..573916ddcc 100644
--- a/theories/Bool/IfProp.v
+++ b/theories/Bool/IfProp.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Bool.
 
 Inductive IfProp (A B:Prop) : bool -> Prop :=
diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v
index 06ab77cfbb..a34c49175e 100644
--- a/theories/Bool/Sumbool.v
+++ b/theories/Bool/Sumbool.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (** Here are collected some results about the type sumbool (see INIT/Specif.v)
    [sumbool A B], which is written [{A}+{B}], is the informative
    disjunction "A or B", where A and B are logical propositions.
diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v
index 5e9d4afa64..fde0530267 100644
--- a/theories/Bool/Zerob.v
+++ b/theories/Bool/Zerob.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Arith.
 Require Import Bool.