Coq headers + $ in theories/Numbers files

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

7 files changed, 25 insertions, 7 deletions

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.