Imported Upstream version 8.3.pl3upstream/8.3.pl3

58 files changed, 113 insertions, 113 deletions

diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v
index 212eea7a..092eafa3 100644
--- a/theories/Reals/Alembert.v
+++ b/theories/Reals/Alembert.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Alembert.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Alembert.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v
index de9f8827..cab14704 100644
--- a/theories/Reals/AltSeries.v
+++ b/theories/Reals/AltSeries.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-  (*i $Id: AltSeries.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+  (*i $Id: AltSeries.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v
index 84fa8fe1..c378a2e2 100644
--- a/theories/Reals/ArithProp.v
+++ b/theories/Reals/ArithProp.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-  (*i $Id: ArithProp.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+  (*i $Id: ArithProp.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rbasic_fun.
diff --git a/theories/Reals/Binomial.v b/theories/Reals/Binomial.v
index ab352910..55c30aec 100644
--- a/theories/Reals/Binomial.v
+++ b/theories/Reals/Binomial.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-  (*i $Id: Binomial.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+  (*i $Id: Binomial.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/Cauchy_prod.v b/theories/Reals/Cauchy_prod.v
index 279fd3d1..1a2e5eca 100644
--- a/theories/Reals/Cauchy_prod.v
+++ b/theories/Reals/Cauchy_prod.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-  (*i $Id: Cauchy_prod.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+  (*i $Id: Cauchy_prod.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v
index e3854afb..32480b0b 100644
--- a/theories/Reals/Cos_plus.v
+++ b/theories/Reals/Cos_plus.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-  (*i $Id: Cos_plus.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+  (*i $Id: Cos_plus.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v
index 99e39169..dec5abd3 100644
--- a/theories/Reals/Cos_rel.v
+++ b/theories/Reals/Cos_rel.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Cos_rel.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Cos_rel.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v
index 66ee4eb0..2cdc121f 100644
--- a/theories/Reals/DiscrR.v
+++ b/theories/Reals/DiscrR.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i        $Id: DiscrR.v 13323 2010-07-24 15:57:30Z herbelin $       i*)
+(*i        $Id: DiscrR.v 14641 2011-11-06 11:59:10Z herbelin $       i*)
 
 Require Import RIneq.
 Require Import Omega.
diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v
index 57198a5e..75ea4755 100644
--- a/theories/Reals/Exp_prop.v
+++ b/theories/Reals/Exp_prop.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Exp_prop.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Exp_prop.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/Integration.v b/theories/Reals/Integration.v
index 569e122a..3199a4f8 100644
--- a/theories/Reals/Integration.v
+++ b/theories/Reals/Integration.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Integration.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Integration.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Export NewtonInt.
 Require Export RiemannInt_SF.
diff --git a/theories/Reals/LegacyRfield.v b/theories/Reals/LegacyRfield.v
index 1528ed64..32b9699d 100644
--- a/theories/Reals/LegacyRfield.v
+++ b/theories/Reals/LegacyRfield.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: LegacyRfield.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: LegacyRfield.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Export Raxioms.
 Require Export LegacyField.
diff --git a/theories/Reals/MVT.v b/theories/Reals/MVT.v
index 87275e7f..36bbb405 100644
--- a/theories/Reals/MVT.v
+++ b/theories/Reals/MVT.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: MVT.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: MVT.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v
index cfd5d561..79060771 100644
--- a/theories/Reals/NewtonInt.v
+++ b/theories/Reals/NewtonInt.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: NewtonInt.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: NewtonInt.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v
index 1e882b7a..e7182312 100644
--- a/theories/Reals/PSeries_reg.v
+++ b/theories/Reals/PSeries_reg.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: PSeries_reg.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: PSeries_reg.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v
index b1c0c4f9..b2a0e574 100644
--- a/theories/Reals/PartSum.v
+++ b/theories/Reals/PartSum.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: PartSum.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: PartSum.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 5c0cf3e7..f02db3d4 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -1,13 +1,13 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: RIneq.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: RIneq.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*********************************************************)
 (** * Basic lemmas for the classical real numbers        *)
diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v
index 85ad4378..4e4fb378 100644
--- a/theories/Reals/RList.v
+++ b/theories/Reals/RList.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: RList.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: RList.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/ROrderedType.v b/theories/Reals/ROrderedType.v
index 07f7f863..87dc07b8 100644
--- a/theories/Reals/ROrderedType.v
+++ b/theories/Reals/ROrderedType.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v
index 946a8833..8cf36c17 100644
--- a/theories/Reals/R_Ifp.v
+++ b/theories/Reals/R_Ifp.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: R_Ifp.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: R_Ifp.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (**********************************************************)
 (** Complements for the reals.Integer and fractional part *)
diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v
index 317f523b..df2267d1 100644
--- a/theories/Reals/R_sqr.v
+++ b/theories/Reals/R_sqr.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: R_sqr.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: R_sqr.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rbasic_fun.
diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v
index 6eab48c0..26980c95 100644
--- a/theories/Reals/R_sqrt.v
+++ b/theories/Reals/R_sqrt.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: R_sqrt.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: R_sqrt.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v
index 885d97ac..39c2271b 100644
--- a/theories/Reals/Ranalysis.v
+++ b/theories/Reals/Ranalysis.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Ranalysis.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Ranalysis.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v
index def01d6f..673dc3c1 100644
--- a/theories/Reals/Ranalysis1.v
+++ b/theories/Reals/Ranalysis1.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Ranalysis1.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Ranalysis1.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v
index b8610d12..fcff9a01 100644
--- a/theories/Reals/Ranalysis2.v
+++ b/theories/Reals/Ranalysis2.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Ranalysis2.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Ranalysis2.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/Ranalysis3.v b/theories/Reals/Ranalysis3.v
index 1848ca52..c7d95660 100644
--- a/theories/Reals/Ranalysis3.v
+++ b/theories/Reals/Ranalysis3.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Ranalysis3.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Ranalysis3.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v
index 97b6d52b..a7c5a387 100644
--- a/theories/Reals/Ranalysis4.v
+++ b/theories/Reals/Ranalysis4.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Ranalysis4.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Ranalysis4.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index dca2782c..b6286c0d 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Raxioms.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Raxioms.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*********************************************************)
 (**    Axiomatisation of the classical reals             *)
diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v
index ab005daf..23aae957 100644
--- a/theories/Reals/Rbase.v
+++ b/theories/Reals/Rbase.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rbase.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Rbase.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Export Rdefinitions.
 Require Export Raxioms.
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index 39f2bf6f..15b04807 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rbasic_fun.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Rbasic_fun.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*********************************************************)
 (**          Complements for the real numbers            *)
diff --git a/theories/Reals/Rcomplete.v b/theories/Reals/Rcomplete.v
index 6e66e904..f6d40631 100644
--- a/theories/Reals/Rcomplete.v
+++ b/theories/Reals/Rcomplete.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rcomplete.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Rcomplete.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v
index 301e0dcf..d06e2d1b 100644
--- a/theories/Reals/Rdefinitions.v
+++ b/theories/Reals/Rdefinitions.v
@@ -1,11 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(*i $Id: Rdefinitions.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Rdefinitions.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 
 (*********************************************************)
diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v
index 2b8c95f7..701914ac 100644
--- a/theories/Reals/Rderiv.v
+++ b/theories/Reals/Rderiv.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rderiv.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Rderiv.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*********************************************************)
 (**     Definition of the derivative,continuity          *)
diff --git a/theories/Reals/Reals.v b/theories/Reals/Reals.v
index f0ce1353..9929733f 100644
--- a/theories/Reals/Reals.v
+++ b/theories/Reals/Reals.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Reals.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Reals.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (** The library REALS is divided in 6 parts :
    - Rbase: basic lemmas on R
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index f56b68c6..a91cf8ae 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rfunctions.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Rfunctions.v 14641 2011-11-06 11:59:10Z herbelin $ 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 703ecfd4..3ab2bc73 100644
--- a/theories/Reals/Rgeom.v
+++ b/theories/Reals/Rgeom.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rgeom.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Rgeom.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v
index 4534a468..598f5f31 100644
--- a/theories/Reals/RiemannInt.v
+++ b/theories/Reals/RiemannInt.v
@@ -1,13 +1,13 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: RiemannInt.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: RiemannInt.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rfunctions.
 Require Import SeqSeries.
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v
index 976050f7..d0d9519c 100644
--- a/theories/Reals/RiemannInt_SF.v
+++ b/theories/Reals/RiemannInt_SF.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: RiemannInt_SF.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: RiemannInt_SF.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index 72aa9971..d2d935b7 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rlimit.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Rlimit.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*********************************************************)
 (**          Definition of the limit                     *)
diff --git a/theories/Reals/Rlogic.v b/theories/Reals/Rlogic.v
index 0b951ebc..b7ffec2b 100644
--- a/theories/Reals/Rlogic.v
+++ b/theories/Reals/Rlogic.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Reals/Rminmax.v b/theories/Reals/Rminmax.v
index 8f8207d7..c9faee0c 100644
--- a/theories/Reals/Rminmax.v
+++ b/theories/Reals/Rminmax.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Reals/Rpow_def.v b/theories/Reals/Rpow_def.v
index 60fc4ca9..4f7a8d22 100644
--- a/theories/Reals/Rpow_def.v
+++ b/theories/Reals/Rpow_def.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Rpow_def.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: Rpow_def.v 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 Require Import Rdefinitions.
 
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v
index 4c3a04f6..36db12f9 100644
--- a/theories/Reals/Rpower.v
+++ b/theories/Reals/Rpower.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rpower.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Rpower.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 (*i Due to L.Thery i*)
 
 (************************************************************)
diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v
index e4269eb7..947dbb11 100644
--- a/theories/Reals/Rprod.v
+++ b/theories/Reals/Rprod.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rprod.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Rprod.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Compare.
 Require Import Rbase.
diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v
index f7e05fce..db0fddad 100644
--- a/theories/Reals/Rseries.v
+++ b/theories/Reals/Rseries.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rseries.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Rseries.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v
index 4cfca607..fad19ed2 100644
--- a/theories/Reals/Rsigma.v
+++ b/theories/Reals/Rsigma.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rsigma.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Rsigma.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v
index 9f606fe3..f2095982 100644
--- a/theories/Reals/Rsqrt_def.v
+++ b/theories/Reals/Rsqrt_def.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rsqrt_def.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Rsqrt_def.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Sumbool.
 Require Import Rbase.
diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v
index 9b332eea..8e9b2bb3 100644
--- a/theories/Reals/Rtopology.v
+++ b/theories/Reals/Rtopology.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rtopology.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Rtopology.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v
index bdbea3a6..3499ea24 100644
--- a/theories/Reals/Rtrigo.v
+++ b/theories/Reals/Rtrigo.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rtrigo.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Rtrigo.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v
index 9718d20d..de984415 100644
--- a/theories/Reals/Rtrigo_alt.v
+++ b/theories/Reals/Rtrigo_alt.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rtrigo_alt.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Rtrigo_alt.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v
index 9fd7d37c..e5263f9c 100644
--- a/theories/Reals/Rtrigo_calc.v
+++ b/theories/Reals/Rtrigo_calc.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rtrigo_calc.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Rtrigo_calc.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v
index b3c4ca23..417cf13c 100644
--- a/theories/Reals/Rtrigo_def.v
+++ b/theories/Reals/Rtrigo_def.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rtrigo_def.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Rtrigo_def.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/Rtrigo_fun.v b/theories/Reals/Rtrigo_fun.v
index 2cb5eadd..2ed86abe 100644
--- a/theories/Reals/Rtrigo_fun.v
+++ b/theories/Reals/Rtrigo_fun.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rtrigo_fun.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Rtrigo_fun.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v
index 7e771444..59afec88 100644
--- a/theories/Reals/Rtrigo_reg.v
+++ b/theories/Reals/Rtrigo_reg.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rtrigo_reg.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Rtrigo_reg.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v
index f984dc9c..7a1319ea 100644
--- a/theories/Reals/SeqProp.v
+++ b/theories/Reals/SeqProp.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: SeqProp.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: SeqProp.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v
index 35320589..4725fe57 100644
--- a/theories/Reals/SeqSeries.v
+++ b/theories/Reals/SeqSeries.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: SeqSeries.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: SeqSeries.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/SplitAbsolu.v b/theories/Reals/SplitAbsolu.v
index cf050684..67af68d1 100644
--- a/theories/Reals/SplitAbsolu.v
+++ b/theories/Reals/SplitAbsolu.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i      $Id: SplitAbsolu.v 13323 2010-07-24 15:57:30Z herbelin $       i*)
+(*i      $Id: SplitAbsolu.v 14641 2011-11-06 11:59:10Z herbelin $       i*)
 
 Require Import Rbasic_fun.
 
diff --git a/theories/Reals/SplitRmult.v b/theories/Reals/SplitRmult.v
index 6eb10370..85a2cdd0 100644
--- a/theories/Reals/SplitRmult.v
+++ b/theories/Reals/SplitRmult.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: SplitRmult.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: SplitRmult.v 14641 2011-11-06 11:59:10Z herbelin $ 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 9eea1c53..79f39892 100644
--- a/theories/Reals/Sqrt_reg.v
+++ b/theories/Reals/Sqrt_reg.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Sqrt_reg.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Sqrt_reg.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.