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 66ab6f1c8..a1ea2ebc8 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 625cbd194..9a2e738eb 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 d9da08672..b41d65c39 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 90f7ee662..799438d89 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 c2b5ed793..573916ddc 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 06ab77cfb..a34c49175 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 5e9d4afa6..fde053026 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.