30 files changed, 46 insertions, 38 deletions
diff --git a/ide/command_windows.mli b/ide/command_windows.mli
index f3ea7d853..5b060db24 100644
--- a/ide/command_windows.mli
+++ b/ide/command_windows.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 class command_window :
   unit ->
diff --git a/ide/coq.mli b/ide/coq.mli
index 5e2c44de4..1d71db35b 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 open Names
 open Term
diff --git a/ide/coq_tactics.mli b/ide/coq_tactics.mli
index 237468446..c31933baa 100644
--- a/ide/coq_tactics.mli
+++ b/ide/coq_tactics.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 val tactics : string list
 
diff --git a/ide/coqide.mli b/ide/coqide.mli
index 848b45fdb..d84158a0b 100644
--- a/ide/coqide.mli
+++ b/ide/coqide.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* The CoqIde main module. The following function [start] will parse the
    command line, initialize the load path, load the input 
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 091c77a50..ff6614dfb 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 val async : ('a -> unit) -> 'a -> unit
 val browse : (string -> unit) -> string -> unit
diff --git a/ide/preferences.mli b/ide/preferences.mli
index e39bf6704..50b988e90 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 type pref =
     {
diff --git a/ide/undo.mli b/ide/undo.mli
index a49844d1d..82bcf2384 100644
--- a/ide/undo.mli
+++ b/ide/undo.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* An undoable view class *)
 
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index 7fc3dabcd..6e09ce6f0 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 open Names
 
diff --git a/kernel/esubst.mli b/kernel/esubst.mli
index 9f795d857..cd9c16907 100644
--- a/kernel/esubst.mli
+++ b/kernel/esubst.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*s Compact representation of explicit relocations. \\
    [ELSHFT(l,n)] == lift of [n], then apply [lift l].
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index 89491e2f9..0a3220293 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-(*s Mod_subst *)
+(*s [Mod_subst] *)
 
 open Names
 open Term
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index cfcc7bd58..702e79ecc 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Declarations
diff --git a/kernel/vconv.mli b/kernel/vconv.mli
index fa6026509..4aed5d05f 100644
--- a/kernel/vconv.mli
+++ b/kernel/vconv.mli
@@ -1,3 +1,11 @@
+(************************************************************************)
+(*  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*)
 open Names
 open Term
diff --git a/lib/heap.mli b/lib/heap.mli
index de1b6f9ba..0bef2edb2 100644
--- a/lib/heap.mli
+++ b/lib/heap.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Heaps *)
 
diff --git a/lib/predicate.mli b/lib/predicate.mli
index 73e4ecce9..41d5399b9 100644
--- a/lib/predicate.mli
+++ b/lib/predicate.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Module [Pred]: sets over infinite ordered types with complement. *)
 
diff --git a/lib/profile.mli b/lib/profile.mli
index 065cbd0b9..ab2af2398 100644
--- a/lib/profile.mli
+++ b/lib/profile.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*s This program is a small time and allocation profiler for Objective Caml *)
 
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index c961baa01..3ca626121 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 open Pp
 open Environ
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli
index 05f1a81a6..532664274 100644
--- a/parsing/pptactic.mli
+++ b/parsing/pptactic.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 open Pp
 open Genarg
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index fff6808d1..435efa499 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -105,10 +105,10 @@ val map_clb : (constr -> constr) -> clbinding -> clbinding
 (* Unification state *)
 type evar_defs
 
-(* Substitution is not applied to the evar_map *)
+(* Substitution is not applied to the [evar_map] *)
 val subst_evar_defs : substitution -> evar_defs -> evar_defs
 
-(* create an evar_defs with empty meta map: *)
+(* create an [evar_defs] with empty meta map: *)
 val create_evar_defs : evar_map -> evar_defs
 val evars_of         : evar_defs -> evar_map
 val evars_reset_evd  : evar_map ->  evar_defs -> evar_defs
@@ -139,7 +139,7 @@ val get_conv_pbs : evar_defs -> (evar_constraint -> bool) ->
 (* Metas *)
 val meta_list : evar_defs -> (metavariable * clbinding) list
 val meta_defined : evar_defs -> metavariable -> bool
-(* [meta_fvalue] raises Not_found if meta not in map or Anomaly if
+(* [meta_fvalue] raises [Not_found] if meta not in map or [Anomaly] if
    meta has no value *)  
 val meta_fvalue    : evar_defs -> metavariable -> constr freelisted
 val meta_ftype     : evar_defs -> metavariable -> constr freelisted
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index a0b7100b6..7146f7f5e 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 open Names
 open Term
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 12fa2b950..9889fcb0b 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 open Names
 open Topconstr
diff --git a/tactics/equality.mli b/tactics/equality.mli
index f511fe675..4afdfe757 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -30,8 +30,8 @@ val general_rewrite_bindings : bool -> constr with_bindings -> tactic
 val general_rewrite          : bool -> constr -> tactic
 
 (* Obsolete, use [general_rewrite_bindings l2r]
-val rewriteLR_bindings       : constr with_bindings -> tactic
-val rewriteRL_bindings       : constr with_bindings -> tactic
+[val rewriteLR_bindings       : constr with_bindings -> tactic]
+[val rewriteRL_bindings       : constr with_bindings -> tactic]
 *)
 
 (* Equivalent to [general_rewrite l2r] *)
@@ -94,8 +94,8 @@ val substHyp : bool -> types -> identifier -> tactic
    (which, if they fail, raise only UserError, not PatternMatchingFailure)
    or [substClause lr (mkVar id) None]
    or [substClause lr (mkVar id) (Some hyp)]
-val hypSubst_LR : identifier -> clause -> tactic
-val hypSubst_RL : identifier -> clause -> tactic
+[val hypSubst_LR : identifier -> clause -> tactic]
+[val hypSubst_RL : identifier -> clause -> tactic]
 *)
 
 val discriminable : env -> evar_map -> constr -> constr -> bool
diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli
index 7d9a32380..89c5e58b8 100644
--- a/tactics/evar_tactics.mli
+++ b/tactics/evar_tactics.mli
@@ -15,8 +15,8 @@ open Tacexpr
 val instantiate : int -> Rawterm.rawconstr -> 
   (identifier * hyp_location_flag, unit) location -> tactic
 
-(*
+(*i
 val instantiate_tac : tactic_arg list -> tactic
-*)
+i*)
 
 val let_evar : name -> Term.types -> tactic
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index ec3a990ac..cc1db7eb3 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 open Tacexpr
 open Term
diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli
index 34da41ebb..9431a6871 100644
--- a/tactics/extratactics.mli
+++ b/tactics/extratactics.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 open Names
 open Term
diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli
index 426ff6edd..09fb39da8 100644
--- a/tactics/setoid_replace.mli
+++ b/tactics/setoid_replace.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 open Term
 open Proof_type
@@ -25,8 +25,8 @@ type relation =
    }
 
 type 'a relation_class =
-   Relation of 'a    (* the rel_aeq of the relation or the relation*)
- | Leibniz of constr option  (* the carrier (if eq is partially instantiated)*)
+   Relation of 'a    (* the [rel_aeq] of the relation or the relation*)
+ | Leibniz of constr option  (* the [carrier] (if [eq] is partially instantiated)*)
 
 type 'a morphism =
     { args : (bool option * 'a relation_class) list;
@@ -47,7 +47,7 @@ val print_setoids : unit -> unit
 val equiv_list : unit -> constr list
 val default_relation_for_carrier :
   ?filter:(relation -> bool) -> types -> relation relation_class 
-(* [default_morphism] raises Not_found *)
+(* [default_morphism] raises [Not_found] *)
 val default_morphism :
   ?filter:(constr morphism -> bool) -> constr -> relation morphism
 
diff --git a/toplevel/recordobj.mli b/toplevel/recordobj.mli
index 7bc81c5c6..02c3126dd 100755
--- a/toplevel/recordobj.mli
+++ b/toplevel/recordobj.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 val objdef_declare : Libnames.global_reference -> unit
 val add_object_hook : Tacexpr.declaration_hook
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 1c2828af3..0ab5f8ac9 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 open Util
 open Names
diff --git a/translate/ppconstrnew.mli b/translate/ppconstrnew.mli
index 09e21e1ce..9ebdbfb8e 100644
--- a/translate/ppconstrnew.mli
+++ b/translate/ppconstrnew.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
  
-(* $Id$ *)
+(*i $Id$ i*)
 
 open Pp
 open Environ
diff --git a/translate/pptacticnew.mli b/translate/pptacticnew.mli
index 5f89662c7..b2e8942ad 100644
--- a/translate/pptacticnew.mli
+++ b/translate/pptacticnew.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
  
-(* $Id$ *)
+(*i $Id$ i*)
 
 open Pp
 open Genarg
diff --git a/translate/ppvernacnew.mli b/translate/ppvernacnew.mli
index bcd2a7e2b..1b1639939 100644
--- a/translate/ppvernacnew.mli
+++ b/translate/ppvernacnew.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
  
-(* $Id$ *)
+(*i $Id$ i*)
 
 open Pp
 open Genarg