Mise de (*i autour CVS info

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

42 files changed, 177 insertions, 30 deletions

diff --git a/theories/IntMap/Adalloc.v b/theories/IntMap/Adalloc.v
index 47cff4f8e9..63c2f2ad4b 100644
--- a/theories/IntMap/Adalloc.v
+++ b/theories/IntMap/Adalloc.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 Require Bool.
 Require Sumbool.
diff --git a/theories/IntMap/Addec.v b/theories/IntMap/Addec.v
index 889c38d950..abbe450816 100644
--- a/theories/IntMap/Addec.v
+++ b/theories/IntMap/Addec.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 (*s Equality on adresses *)
 Require Bool.
diff --git a/theories/IntMap/Addr.v b/theories/IntMap/Addr.v
index 1623e914b0..debaed16cf 100644
--- a/theories/IntMap/Addr.v
+++ b/theories/IntMap/Addr.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 (*s Representation of adresses by [positive] the type of binary numbers *)
 
diff --git a/theories/IntMap/Adist.v b/theories/IntMap/Adist.v
index f8bae6853c..f5d40e66f8 100644
--- a/theories/IntMap/Adist.v
+++ b/theories/IntMap/Adist.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 Require Bool.
 Require ZArith.
diff --git a/theories/IntMap/Allmaps.v b/theories/IntMap/Allmaps.v
index 89520483ba..fcd111694d 100644
--- a/theories/IntMap/Allmaps.v
+++ b/theories/IntMap/Allmaps.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 Require Export Addr.
 Require Export Adist.
diff --git a/theories/IntMap/Fset.v b/theories/IntMap/Fset.v
index 743c703b27..130e89edc4 100644
--- a/theories/IntMap/Fset.v
+++ b/theories/IntMap/Fset.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 (*s Sets operations on maps *)
 
diff --git a/theories/IntMap/Lsort.v b/theories/IntMap/Lsort.v
index 63a2afa61e..7f8e61e600 100644
--- a/theories/IntMap/Lsort.v
+++ b/theories/IntMap/Lsort.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 Require Bool.
 Require Sumbool.
diff --git a/theories/IntMap/Map.v b/theories/IntMap/Map.v
index ca436cddb5..a9093f08d7 100644
--- a/theories/IntMap/Map.v
+++ b/theories/IntMap/Map.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 (*s Definition of finite sets as trees indexed by adresses *)
 
diff --git a/theories/IntMap/Mapaxioms.v b/theories/IntMap/Mapaxioms.v
index 638a833d7c..957f25e1f0 100644
--- a/theories/IntMap/Mapaxioms.v
+++ b/theories/IntMap/Mapaxioms.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 Require Bool.
 Require Sumbool.
diff --git a/theories/IntMap/Mapc.v b/theories/IntMap/Mapc.v
index 4d9d26ff39..d78c05d6b9 100644
--- a/theories/IntMap/Mapc.v
+++ b/theories/IntMap/Mapc.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 Require Bool.
 Require Sumbool.
diff --git a/theories/IntMap/Mapcanon.v b/theories/IntMap/Mapcanon.v
index b0fc1303db..b1616ebeb8 100644
--- a/theories/IntMap/Mapcanon.v
+++ b/theories/IntMap/Mapcanon.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 Require Bool.
 Require Sumbool.
diff --git a/theories/IntMap/Mapcard.v b/theories/IntMap/Mapcard.v
index ce2a042c99..51c92c2bc5 100644
--- a/theories/IntMap/Mapcard.v
+++ b/theories/IntMap/Mapcard.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 Require Bool.
 Require Sumbool.
diff --git a/theories/IntMap/Mapfold.v b/theories/IntMap/Mapfold.v
index ac959bdd85..46b0fb2c72 100644
--- a/theories/IntMap/Mapfold.v
+++ b/theories/IntMap/Mapfold.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 Require Bool.
 Require Sumbool.
diff --git a/theories/IntMap/Mapiter.v b/theories/IntMap/Mapiter.v
index 43f4ffecaf..39ea1d9d8a 100644
--- a/theories/IntMap/Mapiter.v
+++ b/theories/IntMap/Mapiter.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 Require Bool.
 Require Sumbool.
diff --git a/theories/IntMap/Maplists.v b/theories/IntMap/Maplists.v
index 8a920c68c7..c36c021511 100644
--- a/theories/IntMap/Maplists.v
+++ b/theories/IntMap/Maplists.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 Require Addr.
 Require Addec.
diff --git a/theories/IntMap/Mapsubset.v b/theories/IntMap/Mapsubset.v
index c7cc430bf8..5cbfe7ef76 100644
--- a/theories/IntMap/Mapsubset.v
+++ b/theories/IntMap/Mapsubset.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 Require Bool.
 Require Sumbool.
diff --git a/theories/IntMap/intro.tex b/theories/IntMap/intro.tex
index cfaae2468b..9ad93050c1 100644
--- a/theories/IntMap/intro.tex
+++ b/theories/IntMap/intro.tex
@@ -1,5 +1,6 @@
-\section{IntMap}\label{IntMap}
+\section{Maps indexed by binary integers : IntMap}\label{IntMap}
 
 This library contains a data structure for finite sets implemented by
 an efficient structure of map (trees indexed by binary integers).
+It was initially developed by Jean Goubault.
 
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 50b15b1c9d..4dbab94c15 100755
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(* i$Id$ i*)
 
 (*** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED *)
 
diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v
index 9af874a3fb..675a346e22 100644
--- a/theories/Lists/ListSet.v
+++ b/theories/Lists/ListSet.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* A Library for finite sets, implemented as lists *)
 (* A Library with similar interface will soon be available under
diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v
index 267988cdb2..45ee894fa8 100644
--- a/theories/Lists/PolyList.v
+++ b/theories/Lists/PolyList.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 Require Le.
 
diff --git a/theories/Lists/PolyListSyntax.v b/theories/Lists/PolyListSyntax.v
index 7776b7d2e0..4e59d155d9 100644
--- a/theories/Lists/PolyListSyntax.v
+++ b/theories/Lists/PolyListSyntax.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Syntax for list concatenation *)
 Require PolyList.
diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v
index 5bc9dc97e8..9dc01f0a1f 100755
--- a/theories/Lists/Streams.v
+++ b/theories/Lists/Streams.v
@@ -6,9 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
-Implicit Arguments On.
+Set Implicit Arguments.
 
 Section Streams. (* The set of streams : definition *)
 
@@ -166,6 +166,4 @@ Variable a : A.
 CoFixpoint const : (Stream A) := (Cons a const).
 End Constant_Stream.
 
-
-
-Implicit Arguments Off.
+Unset Implicit Arguments.
diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v
index a57681df67..5fbbc93389 100755
--- a/theories/Lists/TheoryList.v
+++ b/theories/Lists/TheoryList.v
@@ -11,7 +11,7 @@
 (* Some programs and results about lists following CAML Manual *)
 
 Require Export PolyList.
-Implicit Arguments On.
+Set Implicit Arguments.
 Chapter Lists.
 
 Variable  A : Set.
diff --git a/theories/Logic/Classical.v b/theories/Logic/Classical.v
index a9c63f0bf2..563bd71221 100755
--- a/theories/Logic/Classical.v
+++ b/theories/Logic/Classical.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Classical Logic *)
 
diff --git a/theories/Logic/Classical_Pred_Set.v b/theories/Logic/Classical_Pred_Set.v
index 098ae33fce..1fc5b7537c 100755
--- a/theories/Logic/Classical_Pred_Set.v
+++ b/theories/Logic/Classical_Pred_Set.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Classical Predicate Logic on Set*)
 
diff --git a/theories/Logic/Classical_Pred_Type.v b/theories/Logic/Classical_Pred_Type.v
index c5c1053783..c4df92323e 100755
--- a/theories/Logic/Classical_Pred_Type.v
+++ b/theories/Logic/Classical_Pred_Type.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Classical Predicate Logic on Type *)
 
diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v
index 826d068aef..8e003d64c5 100755
--- a/theories/Logic/Classical_Prop.v
+++ b/theories/Logic/Classical_Prop.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Classical Propositional Logic *)
 
diff --git a/theories/Logic/Classical_Type.v b/theories/Logic/Classical_Type.v
index ca63074d85..c5f17117cd 100755
--- a/theories/Logic/Classical_Type.v
+++ b/theories/Logic/Classical_Type.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Classical Logic for Type *)
 
diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v
index 2de8a09617..ca4ba0e1a8 100644
--- a/theories/Logic/Decidable.v
+++ b/theories/Logic/Decidable.v
@@ -1,3 +1,14 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
+
+(* Properties of decidable propositions *)
+
 Definition decidable := [P:Prop] P \/ ~P.
 
 Theorem dec_not_not : (P:Prop)(decidable P) -> (~P -> False) -> P.
diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v
index 01702cd16c..d021fa687e 100755
--- a/theories/Logic/Eqdep.v
+++ b/theories/Logic/Eqdep.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 Section Dependent_Equality.
 
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index a35993acdf..f362eb23ca 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* We prove that there is only one proof of [x=x], i.e [(refl_equal ? x)].
    This holds if the equality upon the set of [x] is decidable.
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 2f8eda34f5..0bee9226eb 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -1,4 +1,13 @@
-(*s John Major's Equality - C. Mc Bride *)
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
+
+(*s John Major's Equality as proposed by C. Mc Bride *)
 
 Set Implicit Arguments.
 
diff --git a/theories/Logic/intro.tex b/theories/Logic/intro.tex
index 23f43a78c4..1fb294f2f5 100755
--- a/theories/Logic/intro.tex
+++ b/theories/Logic/intro.tex
@@ -3,6 +3,6 @@
 This library deals with classical logic and its properties.
 The main file is {\tt Classical.v}.
 
-This library also provides some facts on an equality which contains its
-own proof. See the file {\tt Eqdep.v}.
+This library also provides some facts on equalities for dependent
+types. See the files {\tt Eqdep.v} and {\tt JMeq.v}.
 
diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v
index e766b35d70..a6ac4c922b 100644
--- a/theories/Reals/R_Ifp.v
+++ b/theories/Reals/R_Ifp.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*********************************************************)
 (* Complements for the reals.Integer and fractional part *)
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index 9edaa4d376..1d96ad00de 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*********************************************************)
 (*           Complements for the real numbers            *)
diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v
index 055cf58f86..1bd1e5ec7d 100644
--- a/theories/Reals/Rdefinitions.v
+++ b/theories/Reals/Rdefinitions.v
@@ -5,7 +5,7 @@
 (*    //   *      This file is distributed under the terms of the      *)
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
-(* $Id$ *)
+(*i $Id$ i*)
 
 
 (*********************************************************)
diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v
index 3090feef0b..ce3290de3b 100644
--- a/theories/Reals/Rderiv.v
+++ b/theories/Reals/Rderiv.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*********************************************************)
 (*      Definition of the derivative,continuity          *)
diff --git a/theories/Reals/Reals.v b/theories/Reals/Reals.v
index f623504aa1..01177db2ca 100644
--- a/theories/Reals/Reals.v
+++ b/theories/Reals/Reals.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 Require Export Rdefinitions.
 Require Export TypeSyntax.
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 910fda861b..951c4de649 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*********************************************************)
 (*           Definition of the some functions            *)
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index 79fe3bb01f..4cce53ce47 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*********************************************************)
 (*           Definition of the limit                     *)
diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v
index 0be98a38c0..4f4899f402 100644
--- a/theories/Reals/Rsyntax.v
+++ b/theories/Reals/Rsyntax.v
@@ -5,7 +5,7 @@
 (*    //   *      This file is distributed under the terms of the      *)
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
-(* $Id$ *)
+(*i $Id$ i*)
 
 Require Export Rdefinitions.
 
diff --git a/theories/Reals/TypeSyntax.v b/theories/Reals/TypeSyntax.v
index 3d3ad4d7a1..0044e207d7 100644
--- a/theories/Reals/TypeSyntax.v
+++ b/theories/Reals/TypeSyntax.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*********************************************************)
 (*        Or and Exist in Type                           *)