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

55 files changed, 0 insertions, 109 deletions

diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v
index ef75323e08..1b9be07956 100644
--- a/theories/Reals/Alembert.v
+++ b/theories/Reals/Alembert.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Rseries.
diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v
index cccc8ceec1..9c29e26a3b 100644
--- a/theories/Reals/AltSeries.v
+++ b/theories/Reals/AltSeries.v
@@ -6,8 +6,6 @@
   (*         *       GNU Lesser General Public License Version 2.1        *)
   (************************************************************************)
 
-  (*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Rseries.
diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v
index f22ff5cb25..48324e8e8e 100644
--- a/theories/Reals/ArithProp.v
+++ b/theories/Reals/ArithProp.v
@@ -6,8 +6,6 @@
   (*         *       GNU Lesser General Public License Version 2.1        *)
   (************************************************************************)
 
-  (*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rbasic_fun.
 Require Import Even.
diff --git a/theories/Reals/Binomial.v b/theories/Reals/Binomial.v
index 0d34d22c55..d0df984a12 100644
--- a/theories/Reals/Binomial.v
+++ b/theories/Reals/Binomial.v
@@ -6,8 +6,6 @@
   (*         *       GNU Lesser General Public License Version 2.1        *)
   (************************************************************************)
 
-  (*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import PartSum.
diff --git a/theories/Reals/Cauchy_prod.v b/theories/Reals/Cauchy_prod.v
index 6ea0767d09..68a842c9fc 100644
--- a/theories/Reals/Cauchy_prod.v
+++ b/theories/Reals/Cauchy_prod.v
@@ -6,8 +6,6 @@
   (*         *       GNU Lesser General Public License Version 2.1        *)
   (************************************************************************)
 
-  (*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Rseries.
diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v
index 6c08356a75..c5e2c0ed31 100644
--- a/theories/Reals/Cos_plus.v
+++ b/theories/Reals/Cos_plus.v
@@ -6,8 +6,6 @@
   (*         *       GNU Lesser General Public License Version 2.1        *)
   (************************************************************************)
 
-  (*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import SeqSeries.
diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v
index 7a893c53c3..d27e0ae4c6 100644
--- a/theories/Reals/Cos_rel.v
+++ b/theories/Reals/Cos_rel.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import SeqSeries.
diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v
index e037c77b59..0d41b59000 100644
--- a/theories/Reals/DiscrR.v
+++ b/theories/Reals/DiscrR.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i        $Id$       i*)
-
 Require Import RIneq.
 Require Import Omega.
 Open Local Scope R_scope.
diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v
index 1c74f55a0d..287057f0fd 100644
--- a/theories/Reals/Exp_prop.v
+++ b/theories/Reals/Exp_prop.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import SeqSeries.
diff --git a/theories/Reals/Integration.v b/theories/Reals/Integration.v
index 774a0bd5cd..eba81ff9b6 100644
--- a/theories/Reals/Integration.v
+++ b/theories/Reals/Integration.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export NewtonInt.
 Require Export RiemannInt_SF.
 Require Export RiemannInt.
\ No newline at end of file
diff --git a/theories/Reals/LegacyRfield.v b/theories/Reals/LegacyRfield.v
index b33274af92..ca7cb8feab 100644
--- a/theories/Reals/LegacyRfield.v
+++ b/theories/Reals/LegacyRfield.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export Raxioms.
 Require Export LegacyField.
 Import LegacyRing_theory.
diff --git a/theories/Reals/MVT.v b/theories/Reals/MVT.v
index 4037e3dece..72bd62a699 100644
--- a/theories/Reals/MVT.v
+++ b/theories/Reals/MVT.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Ranalysis1.
diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v
index 74bcf7dcd1..0d75a9dee4 100644
--- a/theories/Reals/NewtonInt.v
+++ b/theories/Reals/NewtonInt.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import SeqSeries.
diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v
index 97793386de..80a5b87a83 100644
--- a/theories/Reals/PSeries_reg.v
+++ b/theories/Reals/PSeries_reg.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import SeqSeries.
diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v
index 6a33b80928..e9a224b978 100644
--- a/theories/Reals/PartSum.v
+++ b/theories/Reals/PartSum.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Rseries.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 2b6af10ecf..7c45556054 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -7,8 +7,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (*********************************************************)
 (** * Basic lemmas for the classical real numbers        *)
 (*********************************************************)
diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v
index 545bd68b2c..8cf56cd7bf 100644
--- a/theories/Reals/RList.v
+++ b/theories/Reals/RList.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Open Local Scope R_scope.
diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v
index 57b2c76756..e530070b1a 100644
--- a/theories/Reals/R_Ifp.v
+++ b/theories/Reals/R_Ifp.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (**********************************************************)
 (** Complements for the reals.Integer and fractional part *)
 (*                                                        *)
diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v
index 6460a92719..1cccb88487 100644
--- a/theories/Reals/R_sqr.v
+++ b/theories/Reals/R_sqr.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rbasic_fun.
 Open Local Scope R_scope.
diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v
index 2c43ee9b9e..13232566f1 100644
--- a/theories/Reals/R_sqrt.v
+++ b/theories/Reals/R_sqrt.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Rsqrt_def.
diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v
index 500dd5295d..53267174b1 100644
--- a/theories/Reals/Ranalysis.v
+++ b/theories/Reals/Ranalysis.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Rtrigo.
diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v
index 1516b3384e..a0b10c8911 100644
--- a/theories/Reals/Ranalysis1.v
+++ b/theories/Reals/Ranalysis1.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Export Rlimit.
diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v
index 1d44b3e731..04c00cb301 100644
--- a/theories/Reals/Ranalysis2.v
+++ b/theories/Reals/Ranalysis2.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Ranalysis1.
diff --git a/theories/Reals/Ranalysis3.v b/theories/Reals/Ranalysis3.v
index 3b685cd8a0..28da1c7c4c 100644
--- a/theories/Reals/Ranalysis3.v
+++ b/theories/Reals/Ranalysis3.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Ranalysis1.
diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v
index 1ed3fb7135..abf0b883fd 100644
--- a/theories/Reals/Ranalysis4.v
+++ b/theories/Reals/Ranalysis4.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import SeqSeries.
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index 9715414f5e..1ed75cdb68 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (*********************************************************)
 (**    Axiomatisation of the classical reals             *)
 (*********************************************************)
diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v
index ab1c074748..8843c5e6ea 100644
--- a/theories/Reals/Rbase.v
+++ b/theories/Reals/Rbase.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Export Rdefinitions.
 Require Export Raxioms.
 Require Export RIneq.
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index 7588020c53..2e1bd0797b 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (*********************************************************)
 (**          Complements for the real numbers            *)
 (*                                                       *)
diff --git a/theories/Reals/Rcomplete.v b/theories/Reals/Rcomplete.v
index 27d5c49efb..de32505291 100644
--- a/theories/Reals/Rcomplete.v
+++ b/theories/Reals/Rcomplete.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Rseries.
diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v
index 023cfc93c3..ab6ed8b10a 100644
--- a/theories/Reals/Rdefinitions.v
+++ b/theories/Reals/Rdefinitions.v
@@ -5,8 +5,6 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(*i $Id$ i*)
-
 
 (*********************************************************)
 (**          Definitions for the axiomatization          *)
diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v
index 6413943a90..19ebcd3cb1 100644
--- a/theories/Reals/Rderiv.v
+++ b/theories/Reals/Rderiv.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (*********************************************************)
 (**     Definition of the derivative,continuity          *)
 (*                                                       *)
diff --git a/theories/Reals/Reals.v b/theories/Reals/Reals.v
index d18213db49..de57a5af2a 100644
--- a/theories/Reals/Reals.v
+++ b/theories/Reals/Reals.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (** The library REALS is divided in 6 parts :
    - Rbase: basic lemmas on R
             equalities and inequalities
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 7371c8acf3..6688913694 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (*i Some properties about pow and sum have been made with John Harrison i*)
 (*i Some Lemmas (about pow and powerRZ) have been done by Laurent Thery i*)
 
diff --git a/theories/Reals/Rgeom.v b/theories/Reals/Rgeom.v
index 8890cbb508..dceb98d45f 100644
--- a/theories/Reals/Rgeom.v
+++ b/theories/Reals/Rgeom.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import SeqSeries.
diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v
index 9fd6e00882..abf817d7a1 100644
--- a/theories/Reals/RiemannInt.v
+++ b/theories/Reals/RiemannInt.v
@@ -7,8 +7,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Rfunctions.
 Require Import SeqSeries.
 Require Import Ranalysis.
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v
index f9b1b890f7..f783d1d827 100644
--- a/theories/Reals/RiemannInt_SF.v
+++ b/theories/Reals/RiemannInt_SF.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Ranalysis.
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index 3aaa7300a9..e0f47364fd 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (*********************************************************)
 (**          Definition of the limit                     *)
 (*                                                       *)
diff --git a/theories/Reals/Rpow_def.v b/theories/Reals/Rpow_def.v
index c7d1893be0..f922e25f62 100644
--- a/theories/Reals/Rpow_def.v
+++ b/theories/Reals/Rpow_def.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 Require Import Rdefinitions.
 
 Fixpoint pow (r:R) (n:nat) : R :=
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v
index a4feed8f3e..957466cbe4 100644
--- a/theories/Reals/Rpower.v
+++ b/theories/Reals/Rpower.v
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
 (*i Due to L.Thery i*)
 
 (************************************************************)
diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v
index bb3df6bb8e..4e3f4d0896 100644
--- a/theories/Reals/Rprod.v
+++ b/theories/Reals/Rprod.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Compare.
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v
index 1ed6b03c53..9e51220622 100644
--- a/theories/Reals/Rseries.v
+++ b/theories/Reals/Rseries.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Compare.
diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v
index 9175927029..155577746a 100644
--- a/theories/Reals/Rsigma.v
+++ b/theories/Reals/Rsigma.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Rseries.
diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v
index 33c20355cc..a8f12a6b39 100644
--- a/theories/Reals/Rsqrt_def.v
+++ b/theories/Reals/Rsqrt_def.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Sumbool.
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v
index 5b55896b17..a086cfd46c 100644
--- a/theories/Reals/Rtopology.v
+++ b/theories/Reals/Rtopology.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Ranalysis1.
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v
index 4981d6fdf1..582b6be759 100644
--- a/theories/Reals/Rtrigo.v
+++ b/theories/Reals/Rtrigo.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import SeqSeries.
diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v
index fe2da83911..1cf0944c08 100644
--- a/theories/Reals/Rtrigo_alt.v
+++ b/theories/Reals/Rtrigo_alt.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import SeqSeries.
diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v
index a7fddb4731..33ea1adba0 100644
--- a/theories/Reals/Rtrigo_calc.v
+++ b/theories/Reals/Rtrigo_calc.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import SeqSeries.
diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v
index 9588e44380..265dae9d4f 100644
--- a/theories/Reals/Rtrigo_def.v
+++ b/theories/Reals/Rtrigo_def.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import SeqSeries.
diff --git a/theories/Reals/Rtrigo_fun.v b/theories/Reals/Rtrigo_fun.v
index cb53b5346e..62d8d9f5fd 100644
--- a/theories/Reals/Rtrigo_fun.v
+++ b/theories/Reals/Rtrigo_fun.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import SeqSeries.
diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v
index 5b731488b1..f38e59e824 100644
--- a/theories/Reals/Rtrigo_reg.v
+++ b/theories/Reals/Rtrigo_reg.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import SeqSeries.
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v
index 82647c8378..642e7fc9e2 100644
--- a/theories/Reals/SeqProp.v
+++ b/theories/Reals/SeqProp.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Rseries.
diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v
index dbfc85bb94..dcfadd566d 100644
--- a/theories/Reals/SeqSeries.v
+++ b/theories/Reals/SeqSeries.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Max.
diff --git a/theories/Reals/SplitAbsolu.v b/theories/Reals/SplitAbsolu.v
index 5882f953c4..90048e50d9 100644
--- a/theories/Reals/SplitAbsolu.v
+++ b/theories/Reals/SplitAbsolu.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i      $Id$       i*)
-
 Require Import Rbasic_fun.
 
 Ltac split_case_Rabs :=
diff --git a/theories/Reals/SplitRmult.v b/theories/Reals/SplitRmult.v
index 51e54860d2..322808f9b5 100644
--- a/theories/Reals/SplitRmult.v
+++ b/theories/Reals/SplitRmult.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (*i Lemma mult_non_zero :(r1,r2:R)``r1<>0`` /\ ``r2<>0`` -> ``r1*r2<>0``. i*)
 
 
diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v
index 4f336648b9..3961b8b0ce 100644
--- a/theories/Reals/Sqrt_reg.v
+++ b/theories/Reals/Sqrt_reg.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Ranalysis1.