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

60 files changed, 0 insertions, 120 deletions

diff --git a/theories/Numbers/BigNumPrelude.v b/theories/Numbers/BigNumPrelude.v
index 08da684441..f11fb67b1a 100644
--- a/theories/Numbers/BigNumPrelude.v
+++ b/theories/Numbers/BigNumPrelude.v
@@ -8,8 +8,6 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (** * BigNumPrelude *)
 
 (** Auxillary functions & theorems used for arbitrary precision efficient
diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index af30b0175b..0403722cb3 100644
--- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -8,8 +8,6 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(* $Id$ *)
-
 (** * Signature and specification of a bounded integer structure *)
 
 (** This file specifies how to represent [Z/nZ] when [n=2^d],
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
index b68e89560e..0796d9f49b 100644
--- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v
+++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -8,8 +8,6 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export NZAxioms.
 Require Import BigNumPrelude.
 Require Import DoubleType.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
index aa798e1c7f..81b2c9403f 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
@@ -8,8 +8,6 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Set Implicit Arguments.
 
 Require Import ZArith.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
index 23c62740c8..bf18c1753d 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
@@ -8,8 +8,6 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Set Implicit Arguments.
 
 Require Import ZArith.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
index 49a4f950a8..a640aaf7f9 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
@@ -8,8 +8,6 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Set Implicit Arguments.
 
 Require Import ZArith.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
index 1ce1e81b0c..ae806dd5e4 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
@@ -8,8 +8,6 @@
 (*         Benjamin Gregoire, Laurent Thery, INRIA, 2007                *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Set Implicit Arguments.
 
 Require Import ZArith.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
index 136f96c043..1c4247231f 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
@@ -8,8 +8,6 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Set Implicit Arguments.
 
 Require Import ZArith.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
index 3405b6f4d6..1395caa338 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
@@ -8,8 +8,6 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Set Implicit Arguments.
 
 Require Import ZArith.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
index 6a2a344490..8b978172c0 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
@@ -8,8 +8,6 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Set Implicit Arguments.
 
 Require Import ZArith.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
index e2c6232013..81df55bd44 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
@@ -8,8 +8,6 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Set Implicit Arguments.
 
 Require Import ZArith.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
index a7e556713a..a5610fe783 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
@@ -8,8 +8,6 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Set Implicit Arguments.
 
 Require Import ZArith.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
index 88cbb484fc..da75219a5b 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
@@ -8,8 +8,6 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Set Implicit Arguments.
 
 Require Import ZArith.
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index e2e5b563f2..ca73a9f005 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (** * Int31 numbers defines indeed a cyclic structure : Z/(2^31)Z *)
 
 (**
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index cc224254f8..9b4c25e2c2 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -8,8 +8,6 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import NaryFunctions.
 Require Import Wf_nat.
 Require Export ZArith.
diff --git a/theories/Numbers/Cyclic/Int31/Ring31.v b/theories/Numbers/Cyclic/Int31/Ring31.v
index a9c499fb95..01002656df 100644
--- a/theories/Numbers/Cyclic/Int31/Ring31.v
+++ b/theories/Numbers/Cyclic/Int31/Ring31.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (** * Int31 numbers defines Z/(2^31)Z, and can hence be equipped
       with a ring structure and a ring tactic *)
 
diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
index da0be5e2ab..a2ee248ab0 100644
--- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v
+++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 (** * Type [Z] viewed modulo a particular constant corresponds to [Z/nZ]
       as defined abstractly in CyclicAxioms. *)
 
diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v
index 5663408d1b..123c40428b 100644
--- a/theories/Numbers/Integer/Abstract/ZAdd.v
+++ b/theories/Numbers/Integer/Abstract/ZAdd.v
@@ -8,8 +8,6 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export ZBase.
 
 Module ZAddPropFunct (Import Z : ZAxiomsSig').
diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v
index de12993f89..adc8432646 100644
--- a/theories/Numbers/Integer/Abstract/ZAddOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v
@@ -8,8 +8,6 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export ZLt.
 
 Module ZAddOrderPropFunct (Import Z : ZAxiomsSig').
diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index 9158a214da..46f7810ac9 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -8,8 +8,6 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export NZAxioms.
 
 Set Implicit Arguments.
diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index 44bb02ecc6..ca288e6b2a 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -8,8 +8,6 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export Decidable.
 Require Export ZAxioms.
 Require Import NZProperties.
diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v
index 849bf6b407..fdb7c77f66 100644
--- a/theories/Numbers/Integer/Abstract/ZLt.v
+++ b/theories/Numbers/Integer/Abstract/ZLt.v
@@ -8,8 +8,6 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export ZMul.
 
 Module ZOrderPropFunct (Import Z : ZAxiomsSig').
diff --git a/theories/Numbers/Integer/Abstract/ZMul.v b/theories/Numbers/Integer/Abstract/ZMul.v
index 84d840ad20..4a87a54c82 100644
--- a/theories/Numbers/Integer/Abstract/ZMul.v
+++ b/theories/Numbers/Integer/Abstract/ZMul.v
@@ -8,8 +8,6 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export ZAdd.
 
 Module ZMulPropFunct (Import Z : ZAxiomsSig').
diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v
index 99be58ebd8..1952f4e2a1 100644
--- a/theories/Numbers/Integer/Abstract/ZMulOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v
@@ -8,8 +8,6 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export ZAddOrder.
 
 Module Type ZMulOrderPropFunct (Import Z : ZAxiomsSig').
diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v
index 45662d3b66..76451da33f 100644
--- a/theories/Numbers/Integer/Abstract/ZProperties.v
+++ b/theories/Numbers/Integer/Abstract/ZProperties.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export ZAxioms ZMaxMin ZSgnAbs.
 
 (** This functor summarizes all known facts about Z.
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index aa62ae76bf..c0b8074b69 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -8,8 +8,6 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export BigN.
 Require Import ZProperties ZDivFloor ZSig ZSigZAxioms ZMake.
 
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 3196f11ea9..41b1d6e697 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -8,8 +8,6 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import ZArith.
 Require Import BigNumPrelude.
 Require Import NSig.
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index bc1dadcd9e..aa857f3ca7 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -8,8 +8,6 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 
 Require Import ZAxioms ZProperties.
 Require Import BinInt Zcompare Zorder ZArith_dec Zbool.
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 8b5624cdf8..cafcc549e3 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -8,8 +8,6 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import NProperties. (* The most complete file for N *)
 Require Export ZProperties. (* The most complete file for Z *)
 Require Export Ring.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v
index ffa91706f7..ab12e584b6 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSig.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v
@@ -8,8 +8,6 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import ZArith Znumtheory.
 
 Open Scope Z_scope.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index bcecb6a8a2..2c4797969d 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import ZArith ZAxioms ZDivFloor ZSig.
 
 (** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig]
diff --git a/theories/Numbers/NaryFunctions.v b/theories/Numbers/NaryFunctions.v
index 417463ebac..121b33b00e 100644
--- a/theories/Numbers/NaryFunctions.v
+++ b/theories/Numbers/NaryFunctions.v
@@ -8,8 +8,6 @@
 (*          Pierre Letouzey, Jerome Vouillon, PPS, Paris 7, 2008        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Local Open Scope type_scope.
 
 Require Import List.
diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v
index 9535cfdb4a..37a174c48b 100644
--- a/theories/Numbers/NatInt/NZAdd.v
+++ b/theories/Numbers/NatInt/NZAdd.v
@@ -8,8 +8,6 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import NZAxioms NZBase.
 
 Module Type NZAddPropSig
diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v
index 97c122029f..66e9c6ceb7 100644
--- a/theories/Numbers/NatInt/NZAddOrder.v
+++ b/theories/Numbers/NatInt/NZAddOrder.v
@@ -8,8 +8,6 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import NZAxioms NZBase NZMul NZOrder.
 
 Module Type NZAddOrderPropSig (Import NZ : NZOrdAxiomsSig').
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index ee7ee159f4..7cfa62eab1 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -8,8 +8,6 @@
 
 (** Initial Author : Evgeny Makarov, INRIA, 2007 *)
 
-(*i $Id$ i*)
-
 Require Export Equalities Orders NumPrelude GenericMinMax.
 
 (** Axiomatization of a domain with zero, successor, predecessor,
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 18e3b9b921..9f587a1d08 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -8,8 +8,6 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import NZAxioms.
 
 Module Type NZBasePropSig (Import NZ : NZDomainSig').
diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v
index eb06cae03c..7afbee4a42 100644
--- a/theories/Numbers/NatInt/NZDomain.v
+++ b/theories/Numbers/NatInt/NZDomain.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export NumPrelude NZAxioms.
 Require Import NZBase NZOrder NZAddOrder Plus Minus.
 
diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v
index 296bd095f9..c97aa9f3ae 100644
--- a/theories/Numbers/NatInt/NZMul.v
+++ b/theories/Numbers/NatInt/NZMul.v
@@ -8,8 +8,6 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import NZAxioms NZBase NZAdd.
 
 Module Type NZMulPropSig
diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v
index 7b64a69836..acc43fc179 100644
--- a/theories/Numbers/NatInt/NZMulOrder.v
+++ b/theories/Numbers/NatInt/NZMulOrder.v
@@ -8,8 +8,6 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import NZAxioms.
 Require Import NZAddOrder.
 
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 14fa0bfde1..bfbcc2c65c 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -8,8 +8,6 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import NZAxioms NZBase Decidable OrdersTac.
 
 Module Type NZOrderPropSig
diff --git a/theories/Numbers/NatInt/NZProperties.v b/theories/Numbers/NatInt/NZProperties.v
index 125b4f62c1..cc7bfe031f 100644
--- a/theories/Numbers/NatInt/NZProperties.v
+++ b/theories/Numbers/NatInt/NZProperties.v
@@ -8,8 +8,6 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export NZAxioms NZMulOrder.
 
 (** This functor summarizes all known facts about NZ.
diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v
index 9f0b54a6a2..8596412807 100644
--- a/theories/Numbers/Natural/Abstract/NAdd.v
+++ b/theories/Numbers/Natural/Abstract/NAdd.v
@@ -8,8 +8,6 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export NBase.
 
 Module NAddPropFunct (Import N : NAxiomsSig').
diff --git a/theories/Numbers/Natural/Abstract/NAddOrder.v b/theories/Numbers/Natural/Abstract/NAddOrder.v
index 0ce04e54eb..67bc808507 100644
--- a/theories/Numbers/Natural/Abstract/NAddOrder.v
+++ b/theories/Numbers/Natural/Abstract/NAddOrder.v
@@ -8,8 +8,6 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export NOrder.
 
 Module NAddOrderPropFunct (Import N : NAxiomsSig').
diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index 42016ab10b..cd3d8f0a8b 100644
--- a/theories/Numbers/Natural/Abstract/NAxioms.v
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -8,8 +8,6 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export NZAxioms.
 
 Set Implicit Arguments.
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index 842f4bcf23..f26f56d0c5 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -8,8 +8,6 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export Decidable.
 Require Export NAxioms.
 Require Import NZProperties.
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
index 22eb2cb34a..2302e8d357 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -8,8 +8,6 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Bool. (* To get the orb and negb function *)
 Require Import RelationPairs.
 Require Export NStrongRec.
diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v
index 47bf38cbaf..12dcd32587 100644
--- a/theories/Numbers/Natural/Abstract/NIso.v
+++ b/theories/Numbers/Natural/Abstract/NIso.v
@@ -8,8 +8,6 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import NBase.
 
 Module Homomorphism (N1 N2 : NAxiomsSig).
diff --git a/theories/Numbers/Natural/Abstract/NMulOrder.v b/theories/Numbers/Natural/Abstract/NMulOrder.v
index a2162b137f..29d1838c2a 100644
--- a/theories/Numbers/Natural/Abstract/NMulOrder.v
+++ b/theories/Numbers/Natural/Abstract/NMulOrder.v
@@ -8,8 +8,6 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export NAddOrder.
 
 Module NMulOrderPropFunct (Import N : NAxiomsSig').
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index 090c02ecf6..9439e04f5c 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -8,8 +8,6 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export NAdd.
 
 Module NOrderPropFunct (Import N : NAxiomsSig').
diff --git a/theories/Numbers/Natural/Abstract/NProperties.v b/theories/Numbers/Natural/Abstract/NProperties.v
index 9fc9b290e5..eed7cac18d 100644
--- a/theories/Numbers/Natural/Abstract/NProperties.v
+++ b/theories/Numbers/Natural/Abstract/NProperties.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export NAxioms NMaxMin.
 
 (** This functor summarizes all known facts about N.
diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v
index cbbcdbff50..bd666bc8ba 100644
--- a/theories/Numbers/Natural/Abstract/NStrongRec.v
+++ b/theories/Numbers/Natural/Abstract/NStrongRec.v
@@ -8,8 +8,6 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (** This file defined the strong (course-of-value, well-founded) recursion
 and proves its properties *)
 
diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v
index 1df032ea35..7d3117fdb5 100644
--- a/theories/Numbers/Natural/Abstract/NSub.v
+++ b/theories/Numbers/Natural/Abstract/NSub.v
@@ -8,8 +8,6 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export NMulOrder.
 
 Module Type NSubPropFunct (Import N : NAxiomsSig').
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index 5442a56263..20cb01b16b 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -8,8 +8,6 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (*S NMake_gen.ml : this file generates NMake.v *)
 
 
diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v
index 9772e6a1f0..9177b8092c 100644
--- a/theories/Numbers/Natural/BigN/Nbasic.v
+++ b/theories/Numbers/Natural/BigN/Nbasic.v
@@ -8,8 +8,6 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import ZArith.
 Require Import BigNumPrelude.
 Require Import Max.
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index e8651d47cb..ba592507b1 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -8,8 +8,6 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import BinPos Ndiv_def.
 Require Export BinNat.
 Require Import NAxioms NProperties NDiv.
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 80d434bab6..491c33666c 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -8,8 +8,6 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Peano Peano_dec Compare_dec EqNat NAxioms NProperties NDiv.
 
 (** Functions not already defined: div mod *)
diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v
index 3f60cbf1a7..55a6302aa3 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSig.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSig.v
@@ -8,8 +8,6 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import ZArith Znumtheory.
 
 Open Scope Z_scope.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 49a60916aa..8cbd96c1fb 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import ZArith Nnat NAxioms NDiv NSig.
 
 (** * The interface [NSig.NType] implies the interface [NAxiomsSig] *)
diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v
index 32860cd31e..5022c9ae69 100644
--- a/theories/Numbers/NumPrelude.v
+++ b/theories/Numbers/NumPrelude.v
@@ -8,8 +8,6 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export Setoid Morphisms.
 
 Set Implicit Arguments.
diff --git a/theories/Numbers/Rational/SpecViaQ/QSig.v b/theories/Numbers/Rational/SpecViaQ/QSig.v
index 10d0189a32..6466fc5118 100644
--- a/theories/Numbers/Rational/SpecViaQ/QSig.v
+++ b/theories/Numbers/Rational/SpecViaQ/QSig.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import QArith Qpower Qminmax Orders RelationPairs GenericMinMax.
 
 Open Scope Q_scope.