From f73d7c4614d000f068550b5144d80b7eceed58e9 Mon Sep 17 00:00:00 2001 From: pboutill Date: Thu, 29 Apr 2010 09:56:37 +0000 Subject: Move from ocamlweb to ocamdoc to generate mli documentation dev/ocamlweb-doc has been erased. I hope no one still use the "new-parse" it generate. In dev/, make html will generate in dev/html/ "clickable version of mlis". (as the caml standard library) make coq.pdf will generate nearly the same awfull stuff that coq.ps was. make {kernel,lib,parsing,..}.{dot,png} will do the dependancy graph of the given directory. ocamldoc comment syntax is here : http://caml.inria.fr/pub/docs/manual-ocaml/manual029.html The possibility to put graphs in pdf/html seems to be lost. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12969 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/libnames.mli | 66 ++++++++++++++++++++++++++-------------------------- 1 file changed, 33 insertions(+), 33 deletions(-) (limited to 'library/libnames.mli') diff --git a/library/libnames.mli b/library/libnames.mli index 9ee7d0ab5..9da6a0d5c 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -1,22 +1,20 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* constructor val subst_constructor : substitution -> constructor -> constructor * constr val subst_global : substitution -> global_reference -> global_reference * constr -(* Turn a global reference into a construction *) +(** Turn a global reference into a construction *) val constr_of_global : global_reference -> constr -(* Turn a construction denoting a global reference into a global reference; +(** Turn a construction denoting a global reference into a global reference; raise [Not_found] if not a global reference *) val global_of_constr : constr -> global_reference -(* Obsolete synonyms for constr_of_global and global_of_constr *) +(** Obsolete synonyms for constr_of_global and global_of_constr *) val constr_of_reference : global_reference -> constr val reference_of_constr : constr -> global_reference @@ -60,7 +58,7 @@ end module Refset : Set.S with type elt = global_reference module Refmap : Map.S with type key = global_reference -(*s Extended global references *) +(** {6 Extended global references } *) type syndef_name = kernel_name @@ -68,19 +66,19 @@ type extended_global_reference = | TrueGlobal of global_reference | SynDef of syndef_name -(*s Dirpaths *) +(** {6 Dirpaths } *) val pr_dirpath : dir_path -> Pp.std_ppcmds val dirpath_of_string : string -> dir_path val string_of_dirpath : dir_path -> string -(* Pop the suffix of a [dir_path] *) +(** Pop the suffix of a [dir_path] *) val pop_dirpath : dir_path -> dir_path -(* Pop the suffix n times *) +(** Pop the suffix n times *) val pop_dirpath_n : int -> dir_path -> dir_path -(* Give the immediate prefix and basename of a [dir_path] *) +(** Give the immediate prefix and basename of a [dir_path] *) val split_dirpath : dir_path -> dir_path * identifier val add_dirpath_suffix : dir_path -> module_ident -> dir_path @@ -95,18 +93,18 @@ val is_dirpath_prefix_of : dir_path -> dir_path -> bool module Dirset : Set.S with type elt = dir_path module Dirmap : Map.S with type key = dir_path -(*s Full paths are {\em absolute} paths of declarations *) +(** {6 Full paths are {e absolute} paths of declarations } *) type full_path -(* Constructors of [full_path] *) +(** Constructors of [full_path] *) val make_path : dir_path -> identifier -> full_path -(* Destructors of [full_path] *) +(** Destructors of [full_path] *) val repr_path : full_path -> dir_path * identifier val dirpath : full_path -> dir_path val basename : full_path -> identifier -(* Parsing and printing of section path as ["coq_root.module.id"] *) +(** Parsing and printing of section path as ["coq_root.module.id"] *) val path_of_string : string -> full_path val string_of_path : full_path -> string val pr_path : full_path -> std_ppcmds @@ -116,7 +114,7 @@ module Spmap : Map.S with type key = full_path val restrict_path : int -> full_path -> full_path -(*s Temporary function to brutally form kernel names from section paths *) +(** {6 Temporary function to brutally form kernel names from section paths } *) val encode_mind : dir_path -> identifier -> mutual_inductive val decode_mind : mutual_inductive -> dir_path * identifier @@ -124,7 +122,8 @@ val encode_con : dir_path -> identifier -> constant val decode_con : constant -> dir_path * identifier -(*s A [qualid] is a partially qualified ident; it includes fully +(** {6 Sect } *) +(** A [qualid] is a partially qualified ident; it includes fully qualified names (= absolute names) and all intermediate partial qualifications of absolute names, including single identifiers. The [qualid] are used to access the name table. *) @@ -138,14 +137,14 @@ val pr_qualid : qualid -> std_ppcmds val string_of_qualid : qualid -> string val qualid_of_string : string -> qualid -(* Turns an absolute name, a dirpath, or an identifier into a +(** Turns an absolute name, a dirpath, or an identifier into a qualified name denoting the same name *) val qualid_of_path : full_path -> qualid val qualid_of_dirpath : dir_path -> qualid val qualid_of_ident : identifier -> qualid -(* Both names are passed to objects: a "semantic" [kernel_name], which +(** Both names are passed to objects: a "semantic" [kernel_name], which can be substituted and a "syntactic" [full_path] which can be printed *) @@ -155,16 +154,17 @@ 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 | DirOpenSection of object_prefix | DirModule of object_prefix | DirClosedSection of dir_path - (* this won't last long I hope! *) + (** this won't last long I hope! *) -(*s A [reference] is the user-level notion of name. It denotes either a +(** {6 Sect } *) +(** A [reference] is the user-level notion of name. It denotes either a global name (referred either by a qualified name or by a single name) or a variable *) @@ -177,13 +177,13 @@ val string_of_reference : reference -> string val pr_reference : reference -> std_ppcmds val loc_of_reference : reference -> loc -(*s Popping one level of section in global names *) +(** {6 Popping one level of section in global names } *) val pop_con : constant -> constant val pop_kn : mutual_inductive-> mutual_inductive val pop_global_reference : global_reference -> global_reference -(* Deprecated synonyms *) +(** Deprecated synonyms *) -val make_short_qualid : identifier -> qualid (* = qualid_of_ident *) -val qualid_of_sp : full_path -> qualid (* = qualid_of_path *) +val make_short_qualid : identifier -> qualid (** = qualid_of_ident *) +val qualid_of_sp : full_path -> qualid (** = qualid_of_path *) -- cgit v1.2.3