Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient

pas correctes



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

52 files changed, 81 insertions, 47 deletions

diff --git a/contrib/dp/Dp.v b/contrib/dp/Dp.v
index db028a5ea2..47d67725f2 100644
--- a/contrib/dp/Dp.v
+++ b/contrib/dp/Dp.v
@@ -6,7 +6,7 @@ Require Export Classical.
 (* Zenon *)
 
 (*  Copyright 2004 INRIA  *)
-(*  $Id: zenon.v,v 1.6 2006-02-16 09:22:46 doligez Exp $  *)
+(*  $Id$  *)
 
 Lemma zenon_nottrue :
   (~True -> False).
diff --git a/contrib/dp/zenon.v b/contrib/dp/zenon.v
index 2ef9436755..502465c6be 100644
--- a/contrib/dp/zenon.v
+++ b/contrib/dp/zenon.v
@@ -1,5 +1,5 @@
 (*  Copyright 2004 INRIA  *)
-(*  $Id: zenon.v,v 1.6 2006-02-16 09:22:46 doligez Exp $  *)
+(*  $Id$  *)
 
 Require Export Classical.
 
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index 39eaa0b98b..c5f8509759 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -280,7 +280,7 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
     | TacExact          c
     | TacExactNoCheck   c
     | TacVmCastNoCheck  c  -> depends_of_'constr c acc
-    | TacApply (_, cb) -> depends_of_'constr_with_bindings cb acc
+    | TacApply (_, _, cb) -> depends_of_'constr_with_bindings cb acc
     | TacElim (_, cwb, cwbo) ->
 	depends_of_'constr_with_bindings cwb
 	  (Option.fold_right depends_of_'constr_with_bindings cwbo acc)
diff --git a/contrib/ring/LegacyRing.v b/contrib/ring/LegacyRing.v
index dc8635bdf9..ed1da9c56e 100644
--- a/contrib/ring/LegacyRing.v
+++ b/contrib/ring/LegacyRing.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Ring.v 5920 2004-07-16 20:01:26Z herbelin $ *)
+(* $Id$ *)
 
 Require Export Bool.
 Require Export LegacyRing_theory.
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 5b8bb9c0f8..1bc5897c45 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cases.ml 9399 2006-11-22 16:11:53Z herbelin $ *)
+(* $Id$ *)
 
 open Cases
 open Util
diff --git a/contrib/subtac/subtac_cases.mli b/contrib/subtac/subtac_cases.mli
index 02fe016d63..90989d2d31 100644
--- a/contrib/subtac/subtac_cases.mli
+++ b/contrib/subtac/subtac_cases.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: cases.mli 8741 2006-04-26 22:30:32Z herbelin $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Util
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index d652436802..0bff421383 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: classes.mli 6748 2005-02-18 22:17:50Z herbelin $ i*)
+(*i $Id$ i*)
 
 open Pretyping
 open Evd
diff --git a/contrib/subtac/subtac_classes.mli b/contrib/subtac/subtac_classes.mli
index c621f1516f..9a6730454a 100644
--- a/contrib/subtac/subtac_classes.mli
+++ b/contrib/subtac/subtac_classes.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: classes.mli 6748 2005-02-18 22:17:50Z herbelin $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Names
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 0a0e144bd8..2610f10368 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: classes.ml 6748 2005-02-18 22:17:50Z herbelin $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Names
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 9ecdcd6c07..018c471d40 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: classes.ml 6748 2005-02-18 22:17:50Z herbelin $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Names
diff --git a/kernel/byterun/int64_emul.h b/kernel/byterun/int64_emul.h
index ba8a601491..04e38656f3 100644
--- a/kernel/byterun/int64_emul.h
+++ b/kernel/byterun/int64_emul.h
@@ -11,7 +11,7 @@
 /*                                                                     */
 /***********************************************************************/
 
-/* $Id: int64_emul.h,v 1.5 2005/09/22 14:21:50 xleroy Exp $ */
+/* $Id$ */
 
 /* Software emulation of 64-bit integer arithmetic, for C compilers
    that do not support it.  */
diff --git a/kernel/byterun/int64_native.h b/kernel/byterun/int64_native.h
index 2341e99891..f5bef4a6f4 100644
--- a/kernel/byterun/int64_native.h
+++ b/kernel/byterun/int64_native.h
@@ -11,7 +11,7 @@
 /*                                                                     */
 /***********************************************************************/
 
-/* $Id: int64_native.h,v 1.5 2005/09/22 14:21:50 xleroy Exp $ */
+/* $Id$ */
 
 /* Wrapper macros around native 64-bit integer arithmetic,
    so that it has the same interface as the software emulation
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index b82556c78b..44f5dcb32d 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: retroknowledge.ml ??? 2006-??-?? ??:??:??Z spiwack $ *)
+(* $Id$ *)
 
 open Term
 open Names
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 999bf0ede2..2baf382854 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: retroknowledge.mli ??? 2006-??-?? ??:??:??Z spiwack $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Names
diff --git a/kernel/vm.ml b/kernel/vm.ml
index c1d3ca56fd..665e00a305 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -1,3 +1,13 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(* $Id:$ *)
+
 open Names
 open Term
 open Conv_oracle
diff --git a/lib/flags.ml b/lib/flags.ml
index 12b2ed0370..6a801480a2 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: options.ml 10106 2007-08-30 16:56:10Z herbelin $ *)
+(*i $Id:$ i*)
 
 open Util
 
diff --git a/lib/flags.mli b/lib/flags.mli
index 248b59b0df..73962735da 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: options.mli 9679 2007-02-24 15:22:07Z herbelin $ i*)
+(*i $Id$ i*)
 
 (* Global options of the system. *)
 
diff --git a/lib/option.ml b/lib/option.ml
index 95a18396bb..543c108ab9 100644
--- a/lib/option.ml
+++ b/lib/option.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(*i $Id:$ i*)
 
 (** Module implementing basic combinators for OCaml option type.
    It tries follow closely the style of OCaml standard library.
diff --git a/parsing/g_intsyntax.ml b/parsing/g_intsyntax.ml
index b1a8ae3485..4528fde9cb 100644
--- a/parsing/g_intsyntax.ml
+++ b/parsing/g_intsyntax.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $ $ i*)
+(*i $Id:$ i*)
 
 (* digit-based syntax for int31, bigN bigZ and bigQ *)
 
diff --git a/parsing/g_rsyntax.ml b/parsing/g_rsyntax.ml
index 4564790388..3218781d12 100644
--- a/parsing/g_rsyntax.ml
+++ b/parsing/g_rsyntax.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(*i $Id:$ i*)
+
 open Pp
 open Util
 open Names
diff --git a/parsing/g_string_syntax.ml b/parsing/g_string_syntax.ml
index 6d879fb204..6b1faa76ce 100644
--- a/parsing/g_string_syntax.ml
+++ b/parsing/g_string_syntax.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
+(*i $Id:$ i*)
+
 open Pp
 open Util
 open Names
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index b076220b45..64062765a0 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -365,8 +365,12 @@ GEXTEND Gram
       | IDENT "exact_no_check"; c = constr -> TacExactNoCheck c
       | IDENT "vm_cast_no_check"; c = constr -> TacVmCastNoCheck c
 
-      | IDENT "apply"; cl = constr_with_bindings -> TacApply (false,cl)
-      | IDENT "eapply"; cl = constr_with_bindings -> TacApply (true,cl)
+      | IDENT "apply"; cl = constr_with_bindings -> TacApply (true,false,cl)
+      | IDENT "eapply"; cl = constr_with_bindings -> TacApply (true,true,cl)
+      | IDENT "simple"; IDENT "apply"; cl = constr_with_bindings -> 
+          TacApply (false,false,cl)
+      | IDENT "simple"; IDENT "eapply"; cl = constr_with_bindings -> 
+          TacApply (false, true,cl)
       | IDENT "elim"; cl = constr_with_bindings; el = OPT eliminator ->
           TacElim (false,cl,el)
       | IDENT "eelim"; cl = constr_with_bindings; el = OPT eliminator ->
diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4
index 497b8a3c60..44ca8eb2cb 100644
--- a/parsing/q_constr.ml4
+++ b/parsing/q_constr.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
 
-(* $Id: g_constr.ml4,v 1.58 2005/12/30 10:55:32 herbelin Exp $ *)
+(* $Id$ *)
 
 open Rawterm
 open Term
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 922c7af163..55b5315851 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -295,8 +295,8 @@ let rec mlexpr_of_atomic_tactic = function
       <:expr< Tacexpr.TacExactNoCheck $mlexpr_of_constr c$ >>
   | Tacexpr.TacVmCastNoCheck c ->
       <:expr< Tacexpr.TacVmCastNoCheck $mlexpr_of_constr c$ >>
-  | Tacexpr.TacApply (false,cb) ->
-      <:expr< Tacexpr.TacApply False $mlexpr_of_constr_with_binding cb$ >>
+  | Tacexpr.TacApply (b,false,cb) ->
+      <:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_constr_with_binding cb$ >>
   | Tacexpr.TacElim (false,cb,cbo) ->
       let cb = mlexpr_of_constr_with_binding cb in
       let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 9d837df0ee..4c944f4608 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: classes.ml 6748 2005-02-18 22:17:50Z herbelin $ i*)
+(*i $Id:$ i*)
 
 (*i*)
 open Names
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 193f3ae3c2..2646c09dde 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: classes.mli 6748 2005-02-18 22:17:50Z herbelin $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Names
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index ae806cbf57..dc3f81f56f 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: classes.ml 6748 2005-02-18 22:17:50Z herbelin $ i*)
+(*i $Id:$ i*)
 
 (*i*)
 open Names
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index f97aed96a8..d93a354eca 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: classes.mli 6748 2005-02-18 22:17:50Z herbelin $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Names
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index c746e41999..384c4b221d 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -1,3 +1,13 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id:$ i*)
+
 open Names
 open Declarations
 open Term
diff --git a/proofs/decl_mode.ml b/proofs/decl_mode.ml
index b83f9dc658..cdb7b0675e 100644
--- a/proofs/decl_mode.ml
+++ b/proofs/decl_mode.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id:$ *)
+(*i $Id:$ i*)
 
 open Names
 open Term
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 96df8f6418..16bca302e7 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(*i $Id:$ i*)
+
 open Names
 open Constrextern
 open Pp
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 6a8d0d36d3..5c24224774 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -9,7 +9,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: eauto.ml4 10346 2007-12-05 21:11:19Z aspiwack $ *)
+(* $Id$ *)
 
 open Pp
 open Util
diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml
index b33fbde8aa..4eb59a2fb0 100644
--- a/tactics/decl_interp.ml
+++ b/tactics/decl_interp.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(*i $Id:$ i*)
 
 open Util
 open Names
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 014f6ffcd5..5e86abe7bf 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -51,7 +51,7 @@ Abort.
 
 (* Check insertion of coercions in bindings *)
 
-Coercion eq_true : bool >-> Sortclass.
+(*Coercion eq_true : bool >-> Sortclass.*)
 Goal exists A:Prop, A = A.
 exists true.
 trivial.
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index d215bccb9e..fd8576a8cd 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -13,7 +13,7 @@
  * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
  *              91405 Orsay, France *)
 
-(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
+(* $Id$ *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index a4c97fc82d..0ec6c11f99 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -13,7 +13,7 @@
    Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
    91405 Orsay, France *)
 
-(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
+(* $Id$ *)
 
 Require Export Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v
index 4750df6399..64eee17d8e 100644
--- a/theories/Classes/Functions.v
+++ b/theories/Classes/Functions.v
@@ -13,7 +13,7 @@
    Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
    91405 Orsay, France *)
 
-(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
+(* $Id$ *)
 
 Require Import Coq.Classes.RelationClasses.
 Require Import Coq.Classes.Morphisms.
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index cb27fbc380..43320dcebc 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -13,7 +13,7 @@
    Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
    91405 Orsay, France *)
 
-(* $Id: Init.v 616 2007-08-08 12:28:10Z msozeau $ *)
+(* $Id$ *)
 
 (* Ltac typeclass_instantiation := typeclasses eauto || eauto. *)
 
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index c7e199b62b..3a029371b4 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -13,7 +13,7 @@
    Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
    91405 Orsay, France *)
 
-(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
+(* $Id$ *)
 
 Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 0c663b7093..6ef2f756d3 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -14,7 +14,7 @@
    Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
    91405 Orsay, France *)
 
-(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
+(* $Id$ *)
 
 Require Export Coq.Classes.Init.
 Require Import Coq.Program.Basics.
diff --git a/theories/Classes/SetoidAxioms.v b/theories/Classes/SetoidAxioms.v
index 7cf2980c41..17bd4a6d72 100644
--- a/theories/Classes/SetoidAxioms.v
+++ b/theories/Classes/SetoidAxioms.v
@@ -13,7 +13,7 @@
  * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
  *              91405 Orsay, France *)
 
-(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
+(* $Id$ *)
 
 Require Import Coq.Program.Program.
 
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index d370ffa441..f7f460123e 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -13,7 +13,7 @@
    Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
    91405 Orsay, France *)
 
-(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
+(* $Id$ *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 842d32fdbc..639b15f506 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -13,7 +13,7 @@
  * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
  *              91405 Orsay, France *)
 
-(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
+(* $Id$ *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 8d2be43cc8..38bdc0bc92 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -13,7 +13,7 @@
  * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
  *              91405 Orsay, France *)
 
-(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
+(* $Id$ *)
 
 Require Export Coq.Classes.RelationClasses.
 Require Export Coq.Classes.Morphisms.
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index 1129c5b65e..8f1f26dbcd 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -13,7 +13,7 @@
  * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
  *              91405 Orsay, France *)
 
-(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
+(* $Id$ *)
 
 (** The polymorphic identity function. *)
 
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 46a1b5cf25..0f88fbdd93 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Permut.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id$ i*)
 
 (** Tactics related to (dependent) equality and proof irrelevance. *)
 
diff --git a/theories/Program/FunctionalExtensionality.v b/theories/Program/FunctionalExtensionality.v
index c2a6f3df6c..440217bfec 100644
--- a/theories/Program/FunctionalExtensionality.v
+++ b/theories/Program/FunctionalExtensionality.v
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Tactics.v 10410 2007-12-31 13:11:55Z msozeau $ i*)
+(*i $Id$ i*)
 
 (** This module states the axiom of (dependent) functional extensionality and (dependent) eta-expansion.
    It introduces a tactic [extensionality] to apply the axiom of extensionality to an equality goal. 
diff --git a/theories/QArith/Qfield.v b/theories/QArith/Qfield.v
index f54a6c286a..2e51ef9734 100644
--- a/theories/QArith/Qfield.v
+++ b/theories/QArith/Qfield.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Qring.v 9427 2006-12-11 18:46:35Z bgregoir $ i*)
+(*i $Id$ i*)
 
 Require Export Field.
 Require Export QArith_base.
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 05d7857c4e..9feac54111 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(*i $Id:$ i*)
+
 open Tacmach
 open Util
 open Flags
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index eda8760a94..535dda6238 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: classes.ml 6748 2005-02-18 22:17:50Z herbelin $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Names
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index da00044d90..c259971414 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: classes.mli 6748 2005-02-18 22:17:50Z herbelin $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Names
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index fe3bddf376..ae4e8cf52c 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(*i $Id:$ i*)
+
 open Names
 open Mod_subst