Merge commit 'upstream/8.3.pl3+dfsg'

23 files changed, 44 insertions, 44 deletions

diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v
index 0f5ef9d0..2e9dc2de 100644
--- a/theories/Arith/Arith.v
+++ b/theories/Arith/Arith.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: Arith.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Arith.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Export Arith_base.
 Require Export ArithRing.
diff --git a/theories/Arith/Arith_base.v b/theories/Arith/Arith_base.v
index c5135f63..e9953e54 100644
--- a/theories/Arith/Arith_base.v
+++ b/theories/Arith/Arith_base.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: Arith_base.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Arith_base.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Export Le.
 Require Export Lt.
diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
index 2ccf802d..65753e31 100644
--- a/theories/Arith/Between.v
+++ b/theories/Arith/Between.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: Between.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Between.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Le.
 Require Import Lt.
diff --git a/theories/Arith/Bool_nat.v b/theories/Arith/Bool_nat.v
index 9ace38b1..b3dcd8ec 100644
--- a/theories/Arith/Bool_nat.v
+++ b/theories/Arith/Bool_nat.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: Bool_nat.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: Bool_nat.v 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 Require Export Compare_dec.
 Require Export Peano_dec.
diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v
index 2775d132..2fe5c0d9 100644
--- a/theories/Arith/Compare.v
+++ b/theories/Arith/Compare.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: Compare.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Compare.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (** Equality is decidable on [nat] *)
 
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index 0811fea7..99c7415e 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.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: Compare_dec.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Compare_dec.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Le.
 Require Import Lt.
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index adbca442..89620f5f 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.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: Div2.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Div2.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Lt.
 Require Import Plus.
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index e49e5d14..60575beb 100644
--- a/theories/Arith/EqNat.v
+++ b/theories/Arith/EqNat.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: EqNat.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: EqNat.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (** Equality on natural numbers *)
 
diff --git a/theories/Arith/Euclid.v b/theories/Arith/Euclid.v
index 54f4f013..f32e1ad4 100644
--- a/theories/Arith/Euclid.v
+++ b/theories/Arith/Euclid.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: Euclid.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Euclid.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Mult.
 Require Import Compare_dec.
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index 527ad748..5bab97c2 100644
--- a/theories/Arith/Even.v
+++ b/theories/Arith/Even.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: Even.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Even.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (** Here we define the predicates [even] and [odd] by mutual induction
     and we prove the decidability and the exclusion of those predicates.
diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v
index 5385bf61..3b434b96 100644
--- a/theories/Arith/Factorial.v
+++ b/theories/Arith/Factorial.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: Factorial.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Factorial.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Plus.
 Require Import Mult.
diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v
index eda051df..43df01c0 100644
--- a/theories/Arith/Gt.v
+++ b/theories/Arith/Gt.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: Gt.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Gt.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (** Theorems about [gt] in [nat]. [gt] is defined in [Init/Peano.v] as:
 <<
diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
index f24667d0..b73959e7 100644
--- a/theories/Arith/Le.v
+++ b/theories/Arith/Le.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: Le.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Le.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (** Order on natural numbers. [le] is defined in [Init/Peano.v] as:
 <<
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index 0032741e..004274fe 100644
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.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: Lt.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Lt.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (** Theorems about [lt] in nat. [lt] is defined in library [Init/Peano.v] as:
 <<
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v
index b4c4d7ad..d1b1b269 100644
--- a/theories/Arith/Max.v
+++ b/theories/Arith/Max.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: Max.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Max.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (** THIS FILE IS DEPRECATED. Use [MinMax] instead. *)
 
diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v
index 81142249..0c8b5669 100644
--- a/theories/Arith/Min.v
+++ b/theories/Arith/Min.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: Min.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Min.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (** THIS FILE IS DEPRECATED. Use [MinMax] instead. *)
 
diff --git a/theories/Arith/MinMax.v b/theories/Arith/MinMax.v
index 75c13caa..8a23c8f6 100644
--- a/theories/Arith/MinMax.v
+++ b/theories/Arith/MinMax.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/Arith/Minus.v b/theories/Arith/Minus.v
index 39062348..1b36f236 100644
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.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: Minus.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Minus.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (** [minus] (difference between two natural numbers) is defined in [Init/Peano.v] as:
 <<
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index 3ba98472..5dd61d67 100644
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.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: Mult.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Mult.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Export Plus.
 Require Export Minus.
diff --git a/theories/Arith/NatOrderedType.v b/theories/Arith/NatOrderedType.v
index 90ff5b41..fb4bf233 100644
--- a/theories/Arith/NatOrderedType.v
+++ b/theories/Arith/NatOrderedType.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/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index 908f99f0..5cceab8b 100644
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.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: Peano_dec.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Peano_dec.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Decidable.
 
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index 3c5f28b6..12f12300 100644
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/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: Plus.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Plus.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (** Properties of addition. [add] is defined in [Init/Peano.v] as:
 <<
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index 07ab1c3e..23419531 100644
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.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: Wf_nat.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Wf_nat.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (** Well-founded relations and natural numbers *)