summaryrefslogtreecommitdiff
path: root/theories/Numbers/NatInt
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers/NatInt')
-rw-r--r--theories/Numbers/NatInt/NZAdd.v4
-rw-r--r--theories/Numbers/NatInt/NZAddOrder.v4
-rw-r--r--theories/Numbers/NatInt/NZAxioms.v4
-rw-r--r--theories/Numbers/NatInt/NZBase.v4
-rw-r--r--theories/Numbers/NatInt/NZDiv.v2
-rw-r--r--theories/Numbers/NatInt/NZDomain.v4
-rw-r--r--theories/Numbers/NatInt/NZMul.v4
-rw-r--r--theories/Numbers/NatInt/NZMulOrder.v4
-rw-r--r--theories/Numbers/NatInt/NZOrder.v4
-rw-r--r--theories/Numbers/NatInt/NZProperties.v4
10 files changed, 19 insertions, 19 deletions
diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v
index 6f1b879c..782619f0 100644
--- a/theories/Numbers/NatInt/NZAdd.v
+++ b/theories/Numbers/NatInt/NZAdd.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 *)
@@ -8,7 +8,7 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id: NZAdd.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: NZAdd.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
Require Import NZAxioms NZBase.
diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v
index 7c06226f..ed56cd8f 100644
--- a/theories/Numbers/NatInt/NZAddOrder.v
+++ b/theories/Numbers/NatInt/NZAddOrder.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 *)
@@ -8,7 +8,7 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id: NZAddOrder.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: NZAddOrder.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
Require Import NZAxioms NZBase NZMul NZOrder.
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index 389f4eb2..33236cde 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.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 *)
@@ -8,7 +8,7 @@
(** Initial Author : Evgeny Makarov, INRIA, 2007 *)
-(*i $Id: NZAxioms.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: NZAxioms.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
Require Export Equalities Orders NumPrelude GenericMinMax.
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index b5df1669..119f8265 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.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 *)
@@ -8,7 +8,7 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id: NZBase.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: NZBase.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
Require Import NZAxioms.
diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v
index 75f0206f..ba1c171e 100644
--- a/theories/Numbers/NatInt/NZDiv.v
+++ b/theories/Numbers/NatInt/NZDiv.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/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v
index af3e4861..9dba3c3c 100644
--- a/theories/Numbers/NatInt/NZDomain.v
+++ b/theories/Numbers/NatInt/NZDomain.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: NZDomain.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: NZDomain.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
Require Export NumPrelude NZAxioms.
Require Import NZBase NZOrder NZAddOrder Plus Minus.
diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v
index b55f58cb..b1adcea9 100644
--- a/theories/Numbers/NatInt/NZMul.v
+++ b/theories/Numbers/NatInt/NZMul.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 *)
@@ -8,7 +8,7 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id: NZMul.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: NZMul.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
Require Import NZAxioms NZBase NZAdd.
diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v
index dee1a803..09e468ff 100644
--- a/theories/Numbers/NatInt/NZMulOrder.v
+++ b/theories/Numbers/NatInt/NZMulOrder.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 *)
@@ -8,7 +8,7 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id: NZMulOrder.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: NZMulOrder.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
Require Import NZAxioms.
Require Import NZAddOrder.
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 5d7bb701..07805772 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.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 *)
@@ -8,7 +8,7 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id: NZOrder.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: NZOrder.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
Require Import NZAxioms NZBase Decidable OrdersTac.
diff --git a/theories/Numbers/NatInt/NZProperties.v b/theories/Numbers/NatInt/NZProperties.v
index 92dffed3..7279325d 100644
--- a/theories/Numbers/NatInt/NZProperties.v
+++ b/theories/Numbers/NatInt/NZProperties.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 *)
@@ -8,7 +8,7 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id: NZProperties.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: NZProperties.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
Require Export NZAxioms NZMulOrder.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 17:49:19 +0000