Imported Upstream version 8.3.pl3upstream/8.3.pl3

7 files changed, 14 insertions, 14 deletions

diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 8f3c29c6..9509d9fd 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.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: Bool.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Bool.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (** The type [bool] is defined in the prelude as
     [Inductive bool : Set := true : bool | false : bool] *)
diff --git a/theories/Bool/BoolEq.v b/theories/Bool/BoolEq.v
index 9a006e80..ee82caf1 100644
--- a/theories/Bool/BoolEq.v
+++ b/theories/Bool/BoolEq.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: BoolEq.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: BoolEq.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 (* Cuihtlauac Alvarado - octobre 2000 *)
 
 (** Properties of a boolean equality   *)
diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v
index 3f3acccf..daf3a9fb 100644
--- a/theories/Bool/Bvector.v
+++ b/theories/Bool/Bvector.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: Bvector.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Bvector.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (** Bit vectors. Contribution by Jean Duprat (ENS Lyon). *)
 
diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v
index f3123a7a..e49d1f97 100644
--- a/theories/Bool/DecBool.v
+++ b/theories/Bool/DecBool.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: DecBool.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: DecBool.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Set Implicit Arguments.
 
diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v
index dcab1446..9cca05d4 100644
--- a/theories/Bool/IfProp.v
+++ b/theories/Bool/IfProp.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: IfProp.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: IfProp.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Bool.
 
diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v
index 543ff67d..5b1822be 100644
--- a/theories/Bool/Sumbool.v
+++ b/theories/Bool/Sumbool.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: Sumbool.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Sumbool.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (** Here are collected some results about the type sumbool (see INIT/Specif.v)
    [sumbool A B], which is written [{A}+{B}], is the informative
diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v
index a89138d1..e67ba677 100644
--- a/theories/Bool/Zerob.v
+++ b/theories/Bool/Zerob.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: Zerob.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Zerob.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Require Import Arith.
 Require Import Bool.