diff options
Diffstat (limited to 'library')
-rw-r--r-- | library/declaremods.mli | 4 | ||||
-rw-r--r-- | library/lib.mli | 4 | ||||
-rw-r--r-- | library/libnames.mli | 6 | ||||
-rw-r--r-- | library/libobject.mli | 2 | ||||
-rw-r--r-- | library/nameops.mli | 4 | ||||
-rwxr-xr-x | library/nametab.mli | 7 |
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. *) |