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

21 files changed, 0 insertions, 42 deletions

diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v
index 18dbd27f96..0de9136fd0 100644
--- a/theories/Arith/Arith.v
+++ b/theories/Arith/Arith.v
@@ -6,7 +6,5 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export Arith_base.
 Require Export ArithRing.
diff --git a/theories/Arith/Arith_base.v b/theories/Arith/Arith_base.v
index 2d54f0e8d9..9395fc56c2 100644
--- a/theories/Arith/Arith_base.v
+++ b/theories/Arith/Arith_base.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export Le.
 Require Export Lt.
 Require Export Plus.
diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
index 208c257891..b4cdb3c826 100644
--- a/theories/Arith/Between.v
+++ b/theories/Arith/Between.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Le.
 Require Import Lt.
 
diff --git a/theories/Arith/Bool_nat.v b/theories/Arith/Bool_nat.v
index 9fd59e103b..d94a71c9ef 100644
--- a/theories/Arith/Bool_nat.v
+++ b/theories/Arith/Bool_nat.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 Require Export Compare_dec.
 Require Export Peano_dec.
 Require Import Sumbool.
diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v
index 0f2595b266..c401eb283c 100644
--- a/theories/Arith/Compare.v
+++ b/theories/Arith/Compare.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (** Equality is decidable on [nat] *)
 
 Open Local Scope nat_scope.
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index 38d1aef0e6..635b726710 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Le.
 Require Import Lt.
 Require Import Gt.
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index 999a645448..c717e9bf58 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Lt.
 Require Import Plus.
 Require Import Compare_dec.
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index 312b76e97e..7d5b36ae59 100644
--- a/theories/Arith/EqNat.v
+++ b/theories/Arith/EqNat.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (** Equality on natural numbers *)
 
 Open Local Scope nat_scope.
diff --git a/theories/Arith/Euclid.v b/theories/Arith/Euclid.v
index f50dcc84de..f118eb85b9 100644
--- a/theories/Arith/Euclid.v
+++ b/theories/Arith/Euclid.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Mult.
 Require Import Compare_dec.
 Require Import Wf_nat.
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index eaa1bb2d61..fa4414146e 100644
--- a/theories/Arith/Even.v
+++ b/theories/Arith/Even.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (** Here we define the predicates [even] and [odd] by mutual induction
     and we prove the decidability and the exclusion of those predicates.
     The main results about parity are proved in the module Div2. *)
diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v
index 8c53156241..58631a987b 100644
--- a/theories/Arith/Factorial.v
+++ b/theories/Arith/Factorial.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Plus.
 Require Import Mult.
 Require Import Lt.
diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v
index 70169f52a5..20aad5c055 100644
--- a/theories/Arith/Gt.v
+++ b/theories/Arith/Gt.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (** Theorems about [gt] in [nat]. [gt] is defined in [Init/Peano.v] as:
 <<
 Definition gt (n m:nat) := m < n.
diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
index 6140eeb5a3..edf1e34d57 100644
--- a/theories/Arith/Le.v
+++ b/theories/Arith/Le.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (** Order on natural numbers. [le] is defined in [Init/Peano.v] as:
 <<
 Inductive le (n:nat) : nat -> Prop :=
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index af435e54b2..12819940d6 100644
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (** Theorems about [lt] in nat. [lt] is defined in library [Init/Peano.v] as:
 <<
 Definition lt (n m:nat) := S n <= m.
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v
index b94cc24855..ffce727743 100644
--- a/theories/Arith/Max.v
+++ b/theories/Arith/Max.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (** THIS FILE IS DEPRECATED. Use [NPeano.Nat] instead. *)
 
 Require Export NPeano.
diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v
index ba03a40bd4..c980baf09a 100644
--- a/theories/Arith/Min.v
+++ b/theories/Arith/Min.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (** THIS FILE IS DEPRECATED. Use [NPeano.Nat] instead. *)
 
 Require Export NPeano.
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index cd6c0a29e6..490bf8e553 100644
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (** [minus] (difference between two natural numbers) is defined in [Init/Peano.v] as:
 <<
 Fixpoint minus (n m:nat) : nat :=
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index 8346cae38b..811068daf0 100644
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export Plus.
 Require Export Minus.
 Require Export Lt.
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index 42335f98ba..d8b46c78fb 100644
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Decidable.
 
 Open Local Scope nat_scope.
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index 9b7c626156..28613eecc6 100644
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (** Properties of addition. [add] is defined in [Init/Peano.v] as:
 <<
 Fixpoint plus (n m:nat) : nat :=
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index 5bc5d2a584..c12a577f8e 100644
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (** Well-founded relations and natural numbers *)
 
 Require Import Lt.