Prepare upload to squeeze-backportsdebian/8.3.pl3+dfsg-1_bpo60+1

22 files changed, 44 insertions, 44 deletions

diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v
index b20423e0..701d9f8a 100644
--- a/theories/Sets/Classical_sets.v
+++ b/theories/Sets/Classical_sets.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        *)
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Classical_sets.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Classical_sets.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Export Ensembles.
 Require Export Constructive_sets.
diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v
index bb7235ff..d3900446 100644
--- a/theories/Sets/Constructive_sets.v
+++ b/theories/Sets/Constructive_sets.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        *)
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Constructive_sets.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Constructive_sets.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Export Ensembles.
 
diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v
index 8591aef1..c7b496cb 100644
--- a/theories/Sets/Cpo.v
+++ b/theories/Sets/Cpo.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        *)
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Cpo.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Cpo.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Export Ensembles.
 Require Export Relations_1.
diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v
index 1fee462d..6c80ad40 100644
--- a/theories/Sets/Ensembles.v
+++ b/theories/Sets/Ensembles.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        *)
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Ensembles.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Ensembles.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Section Ensembles.
   Variable U : Type.
diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v
index f690e894..09a0a94d 100644
--- a/theories/Sets/Finite_sets.v
+++ b/theories/Sets/Finite_sets.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        *)
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Finite_sets.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Finite_sets.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Ensembles.
 
diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v
index d351cc74..a9fe8ffe 100644
--- a/theories/Sets/Finite_sets_facts.v
+++ b/theories/Sets/Finite_sets_facts.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        *)
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Finite_sets_facts.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Finite_sets_facts.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Export Finite_sets.
 Require Export Constructive_sets.
diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v
index a58e12e6..e5eae17e 100644
--- a/theories/Sets/Image.v
+++ b/theories/Sets/Image.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        *)
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Image.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Image.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Export Finite_sets.
 Require Export Constructive_sets.
diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v
index c85cd8d2..afb9e0e1 100644
--- a/theories/Sets/Infinite_sets.v
+++ b/theories/Sets/Infinite_sets.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        *)
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Infinite_sets.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Infinite_sets.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Export Finite_sets.
 Require Export Constructive_sets.
diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v
index 37173094..5d073a0c 100644
--- a/theories/Sets/Integers.v
+++ b/theories/Sets/Integers.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        *)
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Integers.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Integers.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Export Finite_sets.
 Require Export Constructive_sets.
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v
index 685a680f..6187c08b 100644
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.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: Multiset.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Multiset.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (* G. Huet 1-9-95 *)
 
diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v
index 671c9690..e819cafa 100644
--- a/theories/Sets/Partial_Order.v
+++ b/theories/Sets/Partial_Order.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        *)
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Partial_Order.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Partial_Order.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Export Ensembles.
 Require Export Relations_1.
diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v
index 844989c0..8699eed3 100644
--- a/theories/Sets/Permut.v
+++ b/theories/Sets/Permut.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: Permut.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Permut.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (* G. Huet 1-9-95 *)
 
diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v
index ae9dbb43..372473d6 100644
--- a/theories/Sets/Powerset.v
+++ b/theories/Sets/Powerset.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        *)
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Powerset.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Powerset.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Export Ensembles.
 Require Export Relations_1.
diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v
index f9da4816..66c0c0bb 100644
--- a/theories/Sets/Powerset_Classical_facts.v
+++ b/theories/Sets/Powerset_Classical_facts.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        *)
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Powerset_Classical_facts.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Powerset_Classical_facts.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Export Ensembles.
 Require Export Constructive_sets.
diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v
index ab5bbaf9..09edd08a 100644
--- a/theories/Sets/Powerset_facts.v
+++ b/theories/Sets/Powerset_facts.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        *)
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Powerset_facts.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Powerset_facts.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Export Ensembles.
 Require Export Constructive_sets.
diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v
index 4677219e..2818b370 100644
--- a/theories/Sets/Relations_1.v
+++ b/theories/Sets/Relations_1.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        *)
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Relations_1.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Relations_1.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Section Relations_1.
    Variable U : Type.
diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v
index b6c0df25..f002e926 100644
--- a/theories/Sets/Relations_1_facts.v
+++ b/theories/Sets/Relations_1_facts.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        *)
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Relations_1_facts.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Relations_1_facts.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Export Relations_1.
 
diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v
index 9f7c831c..710bff2b 100644
--- a/theories/Sets/Relations_2.v
+++ b/theories/Sets/Relations_2.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        *)
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Relations_2.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Relations_2.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Export Relations_1.
 
diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v
index 039bae87..5ccdcb11 100644
--- a/theories/Sets/Relations_2_facts.v
+++ b/theories/Sets/Relations_2_facts.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        *)
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Relations_2_facts.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Relations_2_facts.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Export Relations_1.
 Require Export Relations_1_facts.
diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v
index d4a3d87c..1f96a75a 100644
--- a/theories/Sets/Relations_3.v
+++ b/theories/Sets/Relations_3.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        *)
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Relations_3.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Relations_3.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Export Relations_1.
 Require Export Relations_2.
diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v
index 1a22aff9..3a69a231 100644
--- a/theories/Sets/Relations_3_facts.v
+++ b/theories/Sets/Relations_3_facts.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        *)
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Relations_3_facts.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Relations_3_facts.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Export Relations_1.
 Require Export Relations_1_facts.
diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v
index 78da067d..48789f9a 100644
--- a/theories/Sets/Uniset.v
+++ b/theories/Sets/Uniset.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: Uniset.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Uniset.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (** Sets as characteristic functions *)