summaryrefslogtreecommitdiff
path: root/theories/QArith
diff options
context:
space:
mode:
Diffstat (limited to 'theories/QArith')
-rw-r--r--theories/QArith/QArith.v4
-rw-r--r--theories/QArith/QArith_base.v4
-rw-r--r--theories/QArith/QOrderedType.v2
-rw-r--r--theories/QArith/Qabs.v2
-rw-r--r--theories/QArith/Qcanon.v4
-rw-r--r--theories/QArith/Qfield.v4
-rw-r--r--theories/QArith/Qminmax.v2
-rw-r--r--theories/QArith/Qpower.v2
-rw-r--r--theories/QArith/Qreals.v4
-rw-r--r--theories/QArith/Qreduction.v4
-rw-r--r--theories/QArith/Qring.v4
-rw-r--r--theories/QArith/Qround.v2
12 files changed, 19 insertions, 19 deletions
diff --git a/theories/QArith/QArith.v b/theories/QArith/QArith.v
index c7f41de4..2255cd41 100644
--- a/theories/QArith/QArith.v
+++ b/theories/QArith/QArith.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: QArith.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: QArith.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
Require Export QArith_base.
Require Export Qring.
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 6b33c254..18b8823d 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.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: QArith_base.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: QArith_base.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
Require Export ZArith.
Require Export ZArithRing.
diff --git a/theories/QArith/QOrderedType.v b/theories/QArith/QOrderedType.v
index 238de6fa..be894419 100644
--- a/theories/QArith/QOrderedType.v
+++ b/theories/QArith/QOrderedType.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/QArith/Qabs.v b/theories/QArith/Qabs.v
index 53528ec7..747c2c3c 100644
--- a/theories/QArith/Qabs.v
+++ b/theories/QArith/Qabs.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/QArith/Qcanon.v b/theories/QArith/Qcanon.v
index 4a2347d7..71a3b474 100644
--- a/theories/QArith/Qcanon.v
+++ b/theories/QArith/Qcanon.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: Qcanon.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Qcanon.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
Require Import Field.
Require Import QArith.
diff --git a/theories/QArith/Qfield.v b/theories/QArith/Qfield.v
index 0cf5413e..81d59714 100644
--- a/theories/QArith/Qfield.v
+++ b/theories/QArith/Qfield.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: Qfield.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Qfield.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
Require Export Field.
Require Export QArith_base.
diff --git a/theories/QArith/Qminmax.v b/theories/QArith/Qminmax.v
index 01c6ab67..a458fc6e 100644
--- a/theories/QArith/Qminmax.v
+++ b/theories/QArith/Qminmax.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/QArith/Qpower.v b/theories/QArith/Qpower.v
index 765bc45f..9568c796 100644
--- a/theories/QArith/Qpower.v
+++ b/theories/QArith/Qpower.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/QArith/Qreals.v b/theories/QArith/Qreals.v
index 67bb0ffa..8a0ebcff 100644
--- a/theories/QArith/Qreals.v
+++ b/theories/QArith/Qreals.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: Qreals.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Qreals.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
Require Export Rbase.
Require Export QArith_base.
diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v
index 456d305d..eb8c1164 100644
--- a/theories/QArith/Qreduction.v
+++ b/theories/QArith/Qreduction.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: Qreduction.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Qreduction.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
(** Normalisation functions for rational numbers. *)
diff --git a/theories/QArith/Qring.v b/theories/QArith/Qring.v
index 7f7a2d09..173136b8 100644
--- a/theories/QArith/Qring.v
+++ b/theories/QArith/Qring.v
@@ -1,11 +1,11 @@
(************************************************************************)
(* 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: Qring.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Qring.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
Require Export Qfield.
diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v
index 58a7967e..01a97870 100644
--- a/theories/QArith/Qround.v
+++ b/theories/QArith/Qround.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 *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 23:06:30 +0000