Compatibilité ocamlweb pour cible doc

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

6 files changed, 14 insertions, 13 deletions

diff --git a/library/declaremods.mli b/library/declaremods.mli
index 17a97e7ae..5fce1fa48 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -84,7 +84,7 @@ val end_library :
 
 
 (* [really_import_module mp] opens the module [mp] (in a Caml sense).
-   It modifies Nametab and performs the "open_object" function for
+   It modifies Nametab and performs the [open_object] function for
    every object of the module. *)
 
 val really_import_module : module_path -> unit
@@ -108,7 +108,7 @@ val iter_all_segments : bool -> (object_name -> obj -> unit) -> unit
 
 val debug_print_modtab : unit -> Pp.std_ppcmds
 
-(*val debug_print_modtypetab : unit -> Pp.std_ppcmds*)
+(*i val debug_print_modtypetab : unit -> Pp.std_ppcmds i*)
 
 (* For translator *)
 val process_module_bindings : module_ident list ->
diff --git a/library/lib.mli b/library/lib.mli
index fa8a34344..0433897ba 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -60,7 +60,7 @@ val add_leaf : identifier -> obj -> object_name
 val add_absolutely_named_leaf : object_name -> obj -> unit
 val add_anonymous_leaf : obj -> unit
 
-(* this operation adds all objects with the same name and calls load_object 
+(* this operation adds all objects with the same name and calls [load_object]
    for each of them *)
 val add_leaves : identifier -> obj list -> object_name
 
@@ -110,7 +110,7 @@ val start_modtype :
   module_ident -> module_path -> Summary.frozen -> object_prefix
 val end_modtype : module_ident 
   -> object_name * object_prefix * Summary.frozen * library_segment
-(* Lib.add_frozen_state must be called after each of the above functions *)
+(* [Lib.add_frozen_state] must be called after each of the above functions *)
 
 (*s Compilation units *)
 
diff --git a/library/libnames.mli b/library/libnames.mli
index 379ce64b4..8d4ba269d 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -111,8 +111,8 @@ val qualid_of_dirpath : dir_path -> qualid
 
 val make_short_qualid : identifier -> qualid
 
-(* Both names are passed to objects: a "semantic" kernel_name, which
-   can be substituted and a "syntactic" section_path which can be printed
+(* Both names are passed to objects: a "semantic" [kernel_name], which
+   can be substituted and a "syntactic" [section_path] which can be printed
 *)
 
 type object_name = section_path * kernel_name
@@ -121,7 +121,7 @@ type object_prefix = dir_path * (module_path * dir_path)
 
 val make_oname : object_prefix -> identifier -> object_name
 
-(* to this type are mapped dir_path's in the nametab *)
+(* to this type are mapped [dir_path]'s in the nametab *)
 type global_dir_reference = 
   | DirOpenModule of object_prefix
   | DirOpenModtype of object_prefix
diff --git a/library/libobject.mli b/library/libobject.mli
index 562ba0ce4..37447ffbe 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -40,7 +40,7 @@ open Mod_subst
      Keep      - the object is not substitutive, but survives module 
                  closing
      Anticipate - this is for objects which have to be explicitely 
-                 managed by the end_module function (like Require 
+                 managed by the [end_module] function (like Require 
                  and Read markers)
 
      The classification function is also an occasion for a cleanup
diff --git a/library/nameops.mli b/library/nameops.mli
index 257cedfbb..8dd2f6d74 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 open Names
 
@@ -20,7 +20,7 @@ val make_ident : string -> int option -> identifier
 val repr_ident : identifier -> string * int option
 
 val atompart_of_id : identifier -> string  (* remove trailing digits *)
-val root_of_id : identifier -> identifier (* remove trailing digits, ' and _ *)
+val root_of_id : identifier -> identifier (* remove trailing digits, $'$ and $\_$ *)
 
 val add_suffix : identifier -> string -> identifier
 val add_prefix : string -> identifier -> identifier
diff --git a/library/nametab.mli b/library/nametab.mli
index bd6780c8a..81e7c6166 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -33,13 +33,14 @@ open Libnames
 
    \item [locate : qualid -> object_reference]
 
-   Finds the object referred to by [qualid] or raises Not_found 
+   Finds the object referred to by [qualid] or raises [Not_found]
    
-   \item [name_of] : object_reference -> user_name
+   \item [name_of : object_reference -> user_name]
 
    The [user_name] can be for example the shortest non ambiguous [qualid] or 
    the [full_user_name] or [identifier]. Such a function can also have a 
    local context argument. 
+   \end{itemize}
 *)
    
   
@@ -155,7 +156,7 @@ val id_of_global : global_reference -> identifier
 val pr_global_env : Idset.t -> global_reference -> std_ppcmds
 
 
-(* The [shortest_qualid] functions given an object with user_name
+(* The [shortest_qualid] functions given an object with [user_name]
    Coq.A.B.x, try to find the shortest among x, B.x, A.B.x and
    Coq.A.B.x that denotes the same object. *)