Coq headers + $ in theories/Numbers files

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10934 85f007b7-540e-0410-9357-904b9bb8a0f7

57 files changed, 210 insertions, 130 deletions

diff --git a/theories/Numbers/BigNumPrelude.v b/theories/Numbers/BigNumPrelude.v
index 8e4b1d64f..586e50167 100644
--- a/theories/Numbers/BigNumPrelude.v
+++ b/theories/Numbers/BigNumPrelude.v
@@ -1,16 +1,20 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
+(************************************************************************)
 
-(*************************************************************)
-(*      This file is distributed under the terms of the      *)
-(*      GNU Lesser General Public License Version 2.1        *)
-(*************************************************************)
-(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
-(*************************************************************)
+(*i $Id$ i*)
 
-(**********************************************************************
-     Aux.v
+(** * BigNumPrelude *)
+
+(** Auxillary functions & theorems used for arbitrary precision efficient
+    numbers. *)
 
-     Auxillary functions & Theorems
- **********************************************************************)
 
 Require Import ArithRing.
 Require Export ZArith.
diff --git a/theories/Numbers/Cyclic/Abstract/ZnZ.v b/theories/Numbers/Cyclic/Abstract/ZnZ.v
index dfe091209..877e49c11 100644
--- a/theories/Numbers/Cyclic/Abstract/ZnZ.v
+++ b/theories/Numbers/Cyclic/Abstract/ZnZ.v
@@ -5,19 +5,13 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(*        Benjamin Gregoire, INRIA          Laurent Thery, INRIA        *)
+(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
 (* $Id$ *)
 
 (** * Signature and specification of a bounded integer structure *)
 
-(** 
-- Authors: Benjamin Grégoire, Laurent Théry
-- Institution: INRIA
-- Date: 2007
-*)
-
 Set Implicit Arguments.
 
 Require Import ZArith.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/Basic_type.v b/theories/Numbers/Cyclic/DoubleCyclic/Basic_type.v
index 2116aaddd..60fa09584 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/Basic_type.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/Basic_type.v
@@ -5,13 +5,10 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
+(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
+(************************************************************************)
 
-(*************************************************************)
-(*      This file is distributed under the terms of the      *)
-(*      GNU Lesser General Public License Version 2.1        *)
-(*************************************************************)
-(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
-(*************************************************************)
+(*i $Id$ i*)
 
 Set Implicit Arguments.
 
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/GenAdd.v b/theories/Numbers/Cyclic/DoubleCyclic/GenAdd.v
index 889ccaa4d..68703129b 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/GenAdd.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/GenAdd.v
@@ -5,13 +5,10 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
+(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
+(************************************************************************)
 
-(*************************************************************)
-(*      This file is distributed under the terms of the      *)
-(*      GNU Lesser General Public License Version 2.1        *)
-(*************************************************************)
-(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
-(*************************************************************)
+(*i $Id$ i*)
 
 Set Implicit Arguments.
 
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/GenBase.v b/theories/Numbers/Cyclic/DoubleCyclic/GenBase.v
index 2283e3ca0..eb517c060 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/GenBase.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/GenBase.v
@@ -5,17 +5,10 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
+(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
+(************************************************************************)
 
-(* $Id$ *)
-
-(** * *)
-
-(** 
-- Authors: Benjamin Grégoire, Laurent Théry
-- Institution: INRIA
-- Date: 2007
-- Remark: File automatically generated
-*)
+(*i $Id$ i*)
 
 Set Implicit Arguments.
 
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/GenDiv.v b/theories/Numbers/Cyclic/DoubleCyclic/GenDiv.v
index 0e9993b10..057ad3c06 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/GenDiv.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/GenDiv.v
@@ -1,10 +1,14 @@
-
-(*************************************************************)
-(*      This file is distributed under the terms of the      *)
-(*      GNU Lesser General Public License Version 2.1        *)
-(*************************************************************)
-(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
-(*************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*         Benjamin Gregoire, Laurent Thery, INRIA, 2007                *)
+(************************************************************************)
+
+(*i $Id$ i*)
 
 Set Implicit Arguments.
 
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/GenDivn1.v b/theories/Numbers/Cyclic/DoubleCyclic/GenDivn1.v
index a686f0c27..cbf487f4b 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/GenDivn1.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/GenDivn1.v
@@ -1,10 +1,14 @@
-
-(*************************************************************)
-(*      This file is distributed under the terms of the      *)
-(*      GNU Lesser General Public License Version 2.1        *)
-(*************************************************************)
-(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
-(*************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
+(************************************************************************)
+
+(*i $Id$ i*)
 
 Set Implicit Arguments.
 
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/GenLift.v b/theories/Numbers/Cyclic/DoubleCyclic/GenLift.v
index 5f8b00a52..6cc1ecad3 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/GenLift.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/GenLift.v
@@ -1,10 +1,14 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
+(************************************************************************)
 
-(*************************************************************)
-(*      This file is distributed under the terms of the      *)
-(*      GNU Lesser General Public License Version 2.1        *)
-(*************************************************************)
-(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
-(*************************************************************)
+(*i $Id$ i*)
 
 Set Implicit Arguments.
 
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/GenMul.v b/theories/Numbers/Cyclic/DoubleCyclic/GenMul.v
index 57cdeeb88..f42946d6f 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/GenMul.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/GenMul.v
@@ -1,10 +1,14 @@
-
-(*************************************************************)
-(*      This file is distributed under the terms of the      *)
-(*      GNU Lesser General Public License Version 2.1        *)
-(*************************************************************)
-(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
-(*************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
+(************************************************************************)
+
+(*i $Id$ i*)
 
 Set Implicit Arguments.
 
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/GenSqrt.v b/theories/Numbers/Cyclic/DoubleCyclic/GenSqrt.v
index f8cb16858..ce312aa62 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/GenSqrt.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/GenSqrt.v
@@ -1,10 +1,14 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
+(************************************************************************)
 
-(*************************************************************)
-(*      This file is distributed under the terms of the      *)
-(*      GNU Lesser General Public License Version 2.1        *)
-(*************************************************************)
-(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
-(*************************************************************)
+(*i $Id$ i*)
 
 Set Implicit Arguments.
 
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/GenSub.v b/theories/Numbers/Cyclic/DoubleCyclic/GenSub.v
index b96d09562..3babd7716 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/GenSub.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/GenSub.v
@@ -1,10 +1,14 @@
-
-(*************************************************************)
-(*      This file is distributed under the terms of the      *)
-(*      GNU Lesser General Public License Version 2.1        *)
-(*************************************************************)
-(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
-(*************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
+(************************************************************************)
+
+(*i $Id$ i*)
 
 Set Implicit Arguments.
 
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/Zn2Z.v b/theories/Numbers/Cyclic/DoubleCyclic/Zn2Z.v
index 9b77cf039..a70f3c8ec 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/Zn2Z.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/Zn2Z.v
@@ -1,10 +1,14 @@
-
-(*************************************************************)
-(*      This file is distributed under the terms of the      *)
-(*      GNU Lesser General Public License Version 2.1        *)
-(*************************************************************)
-(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
-(*************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
+(************************************************************************)
+
+(*i $Id$ i*)
 
 Set Implicit Arguments.
 
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index d7e80d4a2..032326c81 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -5,8 +5,10 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
+(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
+(************************************************************************)
 
-(*i $ $ i*)
+(*i $Id$ i*)
 
 (* Require Import Notations.*)
 Require Export ZArith.
diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index fdc7bab4c..678781b23 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id$ i*)
 
 Require Export NZAxioms.
 
diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index 0813a3caa..c57f9ede0 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id$ i*)
 
 Require Export Decidable.
 Require Export ZAxioms.
diff --git a/theories/Numbers/Integer/Abstract/ZDomain.v b/theories/Numbers/Integer/Abstract/ZDomain.v
index 51b522a52..ce3ca21c2 100644
--- a/theories/Numbers/Integer/Abstract/ZDomain.v
+++ b/theories/Numbers/Integer/Abstract/ZDomain.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id$ i*)
 
 Require Export NumPrelude.
 
diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v
index 65a938e54..3d21444ad 100644
--- a/theories/Numbers/Integer/Abstract/ZLt.v
+++ b/theories/Numbers/Integer/Abstract/ZLt.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id$ i*)
 
 Require Export ZTimes.
 
diff --git a/theories/Numbers/Integer/Abstract/ZPlus.v b/theories/Numbers/Integer/Abstract/ZPlus.v
index cbe22077e..cdafa1ca7 100644
--- a/theories/Numbers/Integer/Abstract/ZPlus.v
+++ b/theories/Numbers/Integer/Abstract/ZPlus.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id$ i*)
 
 Require Export ZBase.
 
diff --git a/theories/Numbers/Integer/Abstract/ZPlusOrder.v b/theories/Numbers/Integer/Abstract/ZPlusOrder.v
index 079fc356d..3e6421819 100644
--- a/theories/Numbers/Integer/Abstract/ZPlusOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZPlusOrder.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id$ i*)
 
 Require Export ZLt.
 
diff --git a/theories/Numbers/Integer/Abstract/ZTimes.v b/theories/Numbers/Integer/Abstract/ZTimes.v
index 2ff8fd8da..7819dc085 100644
--- a/theories/Numbers/Integer/Abstract/ZTimes.v
+++ b/theories/Numbers/Integer/Abstract/ZTimes.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id$ i*)
 
 Require Export ZPlus.
 
diff --git a/theories/Numbers/Integer/Abstract/ZTimesOrder.v b/theories/Numbers/Integer/Abstract/ZTimesOrder.v
index 0f4cb54a8..6b6f34d75 100644
--- a/theories/Numbers/Integer/Abstract/ZTimesOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZTimesOrder.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id$ i*)
 
 Require Export ZPlusOrder.
 
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 8c7c1f809..934fbc428 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
 Require Export BigN.
 Require Import ZMake.
 
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index da65d276f..5927c2bea 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -5,6 +5,10 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
+(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
+(************************************************************************)
+
+(*i $Id$ i*)
 
 Require Import ZArith.
 Require Import BigNumPrelude.
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index a40832507..3f5583927 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id$ i*)
 
 Require Import NMinus. (* The most complete file for natural numbers *)
 Require Export ZTimesOrder. (* The most complete file for integers *)
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index 6bdfe5642..0d3b251f3 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id$ i*)
 
 Require Export NumPrelude.
 
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 2e5b585bb..0b917e998 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id$ i*)
 
 Require Import NZAxioms.
 
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 133bbde4d..b11b84092 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id$ i*)
 
 Require Import NZAxioms.
 Require Import NZTimes.
diff --git a/theories/Numbers/NatInt/NZPlus.v b/theories/Numbers/NatInt/NZPlus.v
index 7a4c7719b..673b819ba 100644
--- a/theories/Numbers/NatInt/NZPlus.v
+++ b/theories/Numbers/NatInt/NZPlus.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id$ i*)
 
 Require Import NZAxioms.
 Require Import NZBase.
diff --git a/theories/Numbers/NatInt/NZPlusOrder.v b/theories/Numbers/NatInt/NZPlusOrder.v
index 9f1ba0f84..45148bc20 100644
--- a/theories/Numbers/NatInt/NZPlusOrder.v
+++ b/theories/Numbers/NatInt/NZPlusOrder.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id$ i*)
 
 Require Import NZAxioms.
 Require Import NZOrder.
diff --git a/theories/Numbers/NatInt/NZTimes.v b/theories/Numbers/NatInt/NZTimes.v
index 20bd3cdc6..7503ddce2 100644
--- a/theories/Numbers/NatInt/NZTimes.v
+++ b/theories/Numbers/NatInt/NZTimes.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id$ i*)
 
 Require Import NZAxioms.
 Require Import NZPlus.
diff --git a/theories/Numbers/NatInt/NZTimesOrder.v b/theories/Numbers/NatInt/NZTimesOrder.v
index b51e3d22b..b48acc598 100644
--- a/theories/Numbers/NatInt/NZTimesOrder.v
+++ b/theories/Numbers/NatInt/NZTimesOrder.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id$ i*)
 
 Require Import NZAxioms.
 Require Import NZPlusOrder.
diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index 86a828d03..8bd57b988 100644
--- a/theories/Numbers/Natural/Abstract/NAxioms.v
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id$ i*)
 
 Require Export NZAxioms.
 
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index 1a11f7a13..e90977e3d 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id$ i*)
 
 Require Export Decidable.
 Require Export NAxioms.
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
index 027bfd3ce..369c1261c 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
 Require Import Bool. (* To get the orb and negb function *)
 Require Export NStrongRec.
 
diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v
index 4df46e20e..5ad343fe0 100644
--- a/theories/Numbers/Natural/Abstract/NIso.v
+++ b/theories/Numbers/Natural/Abstract/NIso.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id$ i*)
 
 Require Import NBase.
 
diff --git a/theories/Numbers/Natural/Abstract/NMinus.v b/theories/Numbers/Natural/Abstract/NMinus.v
index 5e1d5d8c3..0c24ca984 100644
--- a/theories/Numbers/Natural/Abstract/NMinus.v
+++ b/theories/Numbers/Natural/Abstract/NMinus.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id$ i*)
 
 Require Export NTimesOrder.
 
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index 1e53d8063..bc5753d16 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id$ i*)
 
 Require Export NTimes.
 
diff --git a/theories/Numbers/Natural/Abstract/NPlus.v b/theories/Numbers/Natural/Abstract/NPlus.v
index 09b5a500b..71122e3a5 100644
--- a/theories/Numbers/Natural/Abstract/NPlus.v
+++ b/theories/Numbers/Natural/Abstract/NPlus.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id$ i*)
 
 Require Export NBase.
 
diff --git a/theories/Numbers/Natural/Abstract/NPlusOrder.v b/theories/Numbers/Natural/Abstract/NPlusOrder.v
index 265ea8144..8a8addefc 100644
--- a/theories/Numbers/Natural/Abstract/NPlusOrder.v
+++ b/theories/Numbers/Natural/Abstract/NPlusOrder.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id$ i*)
 
 Require Export NOrder.
 
diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v
index ace608dbe..78b647d99 100644
--- a/theories/Numbers/Natural/Abstract/NStrongRec.v
+++ b/theories/Numbers/Natural/Abstract/NStrongRec.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id$ i*)
 
 (** This file defined the strong (course-of-value, well-founded) recursion
 and proves its properties *)
diff --git a/theories/Numbers/Natural/Abstract/NTimes.v b/theories/Numbers/Natural/Abstract/NTimes.v
index 7d513dc46..8c0132dd9 100644
--- a/theories/Numbers/Natural/Abstract/NTimes.v
+++ b/theories/Numbers/Natural/Abstract/NTimes.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id$ i*)
 
 Require Export NPlus.
 
diff --git a/theories/Numbers/Natural/Abstract/NTimesOrder.v b/theories/Numbers/Natural/Abstract/NTimesOrder.v
index 259416d46..15d99c757 100644
--- a/theories/Numbers/Natural/Abstract/NTimesOrder.v
+++ b/theories/Numbers/Natural/Abstract/NTimesOrder.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id$ i*)
 
 Require Export NPlusOrder.
 
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index b64a853fd..ecb4578eb 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(*i $Id$ i*)
+
 (** * Natural numbers in base 2^31 *)
 
 (**
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index 347485eeb..a180ed1e0 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -5,6 +5,8 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
+(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
+(************************************************************************)
 
 (*i $Id$ i*)
 
@@ -58,15 +60,14 @@ let _ =
   pr "(*    //   *      This file is distributed under the terms of the       *)";
   pr "(*         *       GNU Lesser General Public License Version 2.1        *)";
   pr "(************************************************************************)";
+  pr "(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)";
+  pr "(************************************************************************)";
   pr "";
   pr "(** * NMake *)";
   pr "";
-  pr "(** From a cyclic Z/nZ representation to arbitrary precision natural numbers.";
-  pr "- Authors: Benjamin Grégoire, Laurent Théry";
-  pr "- Institution: INRIA";
-  pr "- Date: 2007";
-  pr "- Remark: File automatically generated by NMake_gen.ml, DO NOT EDIT !";
-  pr "*)";
+  pr "(** From a cyclic Z/nZ representation to arbitrary precision natural numbers.*)";
+  pr "";
+  pr "(** Remark: File automatically generated by NMake_gen.ml, DO NOT EDIT ! *)"; 
   pr "";
   pr "Require Import BigNumPrelude.";
   pr "Require Import ZArith.";
diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v
index 3d20c35ce..9ca078053 100644
--- a/theories/Numbers/Natural/BigN/Nbasic.v
+++ b/theories/Numbers/Natural/BigN/Nbasic.v
@@ -5,6 +5,10 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
+(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
+(************************************************************************)
+
+(*i $Id$ i*)
 
 Require Import ZArith.
 Require Import BigNumPrelude.
diff --git a/theories/Numbers/Natural/Binary/NBinDefs.v b/theories/Numbers/Natural/Binary/NBinDefs.v
index 3110da36a..c2af66724 100644
--- a/theories/Numbers/Natural/Binary/NBinDefs.v
+++ b/theories/Numbers/Natural/Binary/NBinDefs.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id$ i*)
 
 Require Import BinPos.
 Require Export BinNat.
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index bf4432c38..558f2d0e4 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
 Require Export NBinDefs.
 Require Export NArithRing.
 
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 26a6053eb..506cf1df0 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id$ i*)
 
 Require Import Arith.
 Require Import Min.
diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v
index f042ab068..2c221a88e 100644
--- a/theories/Numbers/NumPrelude.v
+++ b/theories/Numbers/NumPrelude.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id$ i*)
 
 Require Export Setoid.
 (*Require Export Bool.*)
diff --git a/theories/Numbers/QRewrite.v b/theories/Numbers/QRewrite.v
index 4fc7ce197..49e0b3e78 100644
--- a/theories/Numbers/QRewrite.v
+++ b/theories/Numbers/QRewrite.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id$ i*)
 
 Require Import List.
 Require Import Setoid.
diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v
index 33e5f669c..c7c7735c0 100644
--- a/theories/Numbers/Rational/BigQ/BigQ.v
+++ b/theories/Numbers/Rational/BigQ/BigQ.v
@@ -5,8 +5,10 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
+(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
+(************************************************************************)
 
-(* *)
+(*i $Id$ i*)
 
 Require Export QMake_base.
 Require Import QpMake.
diff --git a/theories/Numbers/Rational/BigQ/Q0Make.v b/theories/Numbers/Rational/BigQ/Q0Make.v
index e075bdb15..4260c954f 100644
--- a/theories/Numbers/Rational/BigQ/Q0Make.v
+++ b/theories/Numbers/Rational/BigQ/Q0Make.v
@@ -5,6 +5,10 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
+(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
+(************************************************************************)
+
+(*i $Id$ i*)
 
 Require Import Bool.
 Require Import ZArith.
diff --git a/theories/Numbers/Rational/BigQ/QMake_base.v b/theories/Numbers/Rational/BigQ/QMake_base.v
index e12c78581..6c54ed5ad 100644
--- a/theories/Numbers/Rational/BigQ/QMake_base.v
+++ b/theories/Numbers/Rational/BigQ/QMake_base.v
@@ -5,17 +5,13 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
+(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
+(************************************************************************)
 
 (* $Id$ *)
 
 (** * An implementation of rational numbers based on big integers *)
 
-(** 
-- Authors: Benjamin Grégoire, Laurent Théry
-- Institution: INRIA
-- Date: 2007
-*)
-
 Require Export BigN.
 Require Export BigZ.
 
diff --git a/theories/Numbers/Rational/BigQ/QbiMake.v b/theories/Numbers/Rational/BigQ/QbiMake.v
index 8420a5360..8ce671a73 100644
--- a/theories/Numbers/Rational/BigQ/QbiMake.v
+++ b/theories/Numbers/Rational/BigQ/QbiMake.v
@@ -5,6 +5,10 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
+(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
+(************************************************************************)
+
+(*i $Id$ i*)
 
 Require Import Bool.
 Require Import ZArith.
diff --git a/theories/Numbers/Rational/BigQ/QifMake.v b/theories/Numbers/Rational/BigQ/QifMake.v
index 6df06bdf2..436c13758 100644
--- a/theories/Numbers/Rational/BigQ/QifMake.v
+++ b/theories/Numbers/Rational/BigQ/QifMake.v
@@ -5,6 +5,10 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
+(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
+(************************************************************************)
+
+(*i $Id$ i*)
 
 Require Import Bool.
 Require Import ZArith.
diff --git a/theories/Numbers/Rational/BigQ/QpMake.v b/theories/Numbers/Rational/BigQ/QpMake.v
index a194431ec..db6c5926f 100644
--- a/theories/Numbers/Rational/BigQ/QpMake.v
+++ b/theories/Numbers/Rational/BigQ/QpMake.v
@@ -5,6 +5,10 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
+(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
+(************************************************************************)
+
+(*i $Id$ i*)
 
 Require Import Bool.
 Require Import ZArith.
diff --git a/theories/Numbers/Rational/BigQ/QvMake.v b/theories/Numbers/Rational/BigQ/QvMake.v
index 1282c8694..59da4da6d 100644
--- a/theories/Numbers/Rational/BigQ/QvMake.v
+++ b/theories/Numbers/Rational/BigQ/QvMake.v
@@ -5,6 +5,10 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
+(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
+(************************************************************************)
+
+(*i $Id$ i*)
 
 Require Import Bool.
 Require Import ZArith.