Imported Upstream version 8.3.pl3upstream/8.3.pl3

10 files changed, 18 insertions, 18 deletions

diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index cc6e8936..ea1543e3 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.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        *)
@@ -12,7 +12,7 @@
    Institution: LRI, CNRS UMR 8623 - University Paris Sud
 *)
 
-(* $Id: EquivDec.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: EquivDec.v 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 (** Export notations. *)
 
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 3d8c3434..e562328d 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.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        *)
@@ -12,7 +12,7 @@
    Institution: LRI, CNRS UMR 8623 - University Paris Sud
 *)
 
-(* $Id: Equivalence.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: Equivalence.v 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index 8cc1216b..eea16129 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.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        *)
@@ -13,7 +13,7 @@
    Institution: LRI, CNRS UMR 8623 - University Paris Sud
 *)
 
-(* $Id: Init.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: Init.v 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 (** Hints for the proof search: these combinators should be considered rigid. *)
 
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index d31829e1..ea869a66 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -1,7 +1,7 @@
 (* -*- 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        *)
@@ -13,7 +13,7 @@
    Institution: LRI, CNRS UMR 8623 - University Paris Sud
 *)
 
-(* $Id: Morphisms.v 13359 2010-07-30 08:46:55Z herbelin $ *)
+(* $Id: Morphisms.v 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v
index d4ce9aaa..5a2482d4 100644
--- a/theories/Classes/Morphisms_Prop.v
+++ b/theories/Classes/Morphisms_Prop.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/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v
index e962faf0..a8009f9e 100644
--- a/theories/Classes/Morphisms_Relations.v
+++ b/theories/Classes/Morphisms_Relations.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/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 2bfebfd8..94c51bf1 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -1,7 +1,7 @@
 (* -*- 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        *)
@@ -15,7 +15,7 @@
    Institution: LRI, CNRS UMR 8623 - University Paris Sud
 *)
 
-(* $Id: RelationClasses.v 13476 2010-09-30 11:42:11Z letouzey $ *)
+(* $Id: RelationClasses.v 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 Require Export Coq.Classes.Init.
 Require Import Coq.Program.Basics.
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index b20f9d88..e9da6874 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.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        *)
@@ -12,7 +12,7 @@
    Institution: LRI, CNRS UMR 8623 - University Paris Sud
 *)
 
-(* $Id: SetoidClass.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: SetoidClass.v 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index fe775abb..4f70b244 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -1,7 +1,7 @@
 (* -*- 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        *)
@@ -13,7 +13,7 @@
    Institution: LRI, CNRS UMR 8623 - University Paris Sud
 *)
 
-(* $Id: SetoidDec.v 13359 2010-07-30 08:46:55Z herbelin $ *)
+(* $Id: SetoidDec.v 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 0d43de5a..a1a0c969 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.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        *)
@@ -12,7 +12,7 @@
    Institution: LRI, CNRS UMR 8623 - University Paris Sud
 *)
 
-(* $Id: SetoidTactics.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: SetoidTactics.v 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
 Require Export Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions.