summaryrefslogtreecommitdiff
path: root/theories/Bool
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Bool')
-rw-r--r--theories/Bool/Bool.v4
-rw-r--r--theories/Bool/BoolEq.v4
-rw-r--r--theories/Bool/Bvector.v4
-rw-r--r--theories/Bool/DecBool.v4
-rw-r--r--theories/Bool/IfProp.v4
-rw-r--r--theories/Bool/Sumbool.v4
-rw-r--r--theories/Bool/Zerob.v4
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.
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-19 08:34:21 +0000