From 300293c119981054c95182a90c829058530a6b6f Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sun, 25 Dec 2011 13:19:42 +0100
Subject: Imported Upstream version 8.3.pl3

---
 theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v    | 4 ++--
 theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v   | 4 ++--
 theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v | 4 ++--
 theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v    | 4 ++--
 theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v  | 4 ++--
 theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v   | 4 ++--
 theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v    | 4 ++--
 theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v   | 4 ++--
 theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v    | 4 ++--
 theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v   | 4 ++--
 10 files changed, 20 insertions(+), 20 deletions(-)

(limited to 'theories/Numbers/Cyclic/DoubleCyclic')

diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
index f49201d8..305d77a9 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.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 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id: DoubleAdd.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: DoubleAdd.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Set Implicit Arguments.
 
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
index ba2a1770..3d44f96b 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.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 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id: DoubleBase.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: DoubleBase.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Set Implicit Arguments.
 
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
index 4a60a10b..006da1b3 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.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 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id: DoubleCyclic.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: DoubleCyclic.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Set Implicit Arguments.
 
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
index 5ddadd12..4e6eccea 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.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 @@
 (*         Benjamin Gregoire, Laurent Thery, INRIA, 2007                *)
 (************************************************************************)
 
-(*i $Id: DoubleDiv.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: DoubleDiv.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Set Implicit Arguments.
 
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
index 3ada7d40..4bdb75d6 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.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 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id: DoubleDivn1.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: DoubleDivn1.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Set Implicit Arguments.
 
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
index 3989791c..36e3da9b 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.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 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id: DoubleLift.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: DoubleLift.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Set Implicit Arguments.
 
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
index 7ddb0468..834e85d2 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.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 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id: DoubleMul.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: DoubleMul.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Set Implicit Arguments.
 
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
index d468318d..4394178f 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.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 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id: DoubleSqrt.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: DoubleSqrt.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Set Implicit Arguments.
 
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
index 7cb97f28..3167f4c7 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.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 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id: DoubleSub.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: DoubleSub.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Set Implicit Arguments.
 
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
index e9955c6d..eb1132d4 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.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 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id: DoubleType.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: DoubleType.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 Set Implicit Arguments.
 
-- 
cgit v1.2.3