aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/lib.mli
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2005-01-21 17:18:23 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2005-01-21 17:18:23 +0000
commitd7b2414b631d71e89e677d650b84bd4fadd44895 (patch)
tree47b653e7e0ae9b83dbc8a96b2c5be4717b2eefbd /library/lib.mli
parentea6bd4e5496f0fd7e059cd9b924f29ca80a38ae2 (diff)
Compatibilité ocamlweb pour cible doc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6616 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/lib.mli')
-rw-r--r--library/lib.mli4
1 files changed, 2 insertions, 2 deletions
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 *)