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/decl_kinds.mli | 38 +++++++++++----------- library/declare.mli | 40 +++++++++++------------ library/declaremods.mli | 44 +++++++++++++------------ library/decls.mli | 16 ++++----- library/dischargedhypsmap.mli | 21 ++++++------ library/global.mli | 39 +++++++++++----------- library/goptions.mli | 42 ++++++++++++------------ library/heads.mli | 20 ++++++------ library/impargs.mli | 32 +++++++++--------- library/lib.mli | 76 +++++++++++++++++++++++-------------------- library/libnames.mli | 66 ++++++++++++++++++------------------- library/libobject.mli | 25 +++++++------- library/library.mli | 48 ++++++++++++++------------- library/nameops.mli | 28 ++++++++-------- library/nametab.mli | 68 +++++++++++++++++++------------------- library/states.mli | 23 +++++++------ library/summary.mli | 16 ++++----- 17 files changed, 325 insertions(+), 317 deletions(-) (limited to 'library') diff --git a/library/decl_kinds.mli b/library/decl_kinds.mli index 0ebab9ca0..abc201eb1 100644 --- a/library/decl_kinds.mli +++ b/library/decl_kinds.mli @@ -1,17 +1,17 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* logical_kind val string_of_theorem_kind : theorem_kind -> string val string_of_definition_kind : locality * boxed_flag * definition_object_kind -> string -(* About locality *) +(** About locality *) val strength_of_global : global_reference -> locality val string_of_strength : locality -> string -(* About recursive power of type declarations *) +(** About recursive power of type declarations *) type recursivity_kind = - | Finite (* = inductive *) - | CoFinite (* = coinductive *) - | BiFinite (* = non-recursive, like in "Record" definitions *) + | Finite (** = inductive *) + | CoFinite (** = coinductive *) + | BiFinite (** = non-recursive, like in "Record" definitions *) -(* helper, converts to "finiteness flag" booleans *) +(** helper, converts to "finiteness flag" booleans *) val recursivity_flag_of_kind : recursivity_kind -> bool diff --git a/library/declare.mli b/library/declare.mli index 09526f341..1b4564d9c 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -1,14 +1,13 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* variable_declaration -> object_name -(* Declaration of global constructions *) -(* i.e. Definition/Theorem/Axiom/Parameter/... *) +(** Declaration of global constructions + i.e. Definition/Theorem/Axiom/Parameter/... *) type constant_declaration = constant_entry * logical_kind -(* [declare_constant id cd] declares a global declaration +(** [declare_constant id cd] declares a global declaration (constant/parameter) with name [id] in the current section; it returns the full path of the declaration *) val declare_constant : @@ -54,25 +52,25 @@ val declare_constant : val declare_internal_constant : identifier -> constant_declaration -> constant -(* [declare_mind me] declares a block of inductive types with +(** [declare_mind me] declares a block of inductive types with their constructors in the current section; it returns the path of the whole block (boolean must be true iff it is a record) *) val declare_mind : bool -> mutual_inductive_entry -> object_name -(* Hooks for XML output *) +(** Hooks for XML output *) val set_xml_declare_variable : (object_name -> unit) -> unit val set_xml_declare_constant : (bool * constant -> unit) -> unit val set_xml_declare_inductive : (bool * object_name -> unit) -> unit -(* Hook for the cache function of constants and inductives *) +(** Hook for the cache function of constants and inductives *) val add_cache_hook : (full_path -> unit) -> unit -(* Declaration messages *) +(** Declaration messages *) val definition_message : identifier -> unit val assumption_message : identifier -> unit val fixpoint_message : int array option -> identifier list -> unit val cofixpoint_message : identifier list -> unit -val recursive_message : bool (* true = fixpoint *) -> +val recursive_message : bool (** true = fixpoint *) -> int array option -> identifier list -> unit diff --git a/library/declaremods.mli b/library/declaremods.mli index e58f96744..17fd44024 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -1,14 +1,13 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* module_path -(*s Module types *) +(** {6 Module types } *) val declare_modtype : (env -> 'modast -> module_struct_entry) -> (env -> 'modast -> module_struct_entry * bool) -> @@ -67,13 +67,14 @@ val start_modtype : (env -> 'modast -> module_struct_entry) -> val end_modtype : unit -> module_path -(*s Objects of a module. They come in two lists: the substitutive ones +(** {6 Sect } *) +(** Objects of a module. They come in two lists: the substitutive ones and the other *) val module_objects : module_path -> library_segment -(*s Libraries i.e. modules on disk *) +(** {6 Libraries i.e. modules on disk } *) type library_name = dir_path @@ -88,27 +89,28 @@ val start_library : library_name -> unit val end_library : library_name -> Safe_typing.compiled_library * library_objects -(* set a function to be executed at end_library *) +(** set a function to be executed at end_library *) val set_end_library_hook : (unit -> unit) -> unit -(* [really_import_module mp] opens the module [mp] (in a Caml sense). +(** [really_import_module mp] opens the module [mp] (in a Caml sense). It modifies Nametab and performs the [open_object] function for every object of the module. *) val really_import_module : module_path -> unit -(* [import_module export mp] is a synchronous version of +(** [import_module export mp] is a synchronous version of [really_import_module]. If [export] is [true], the module is also opened every time the module containing it is. *) val import_module : bool -> module_path -> unit -(* Include *) +(** Include *) val declare_include : (env -> 'struct_expr -> module_struct_entry * bool) -> ('struct_expr * bool) list -> unit -(*s [iter_all_segments] iterate over all segments, the modules' +(** {6 Sect } *) +(** [iter_all_segments] iterate over all segments, the modules' segments first and then the current segment. Modules are presented in an arbitrary order. The given function is applied to all leaves (together with their section path). *) @@ -120,7 +122,7 @@ val debug_print_modtab : unit -> Pp.std_ppcmds (*i val debug_print_modtypetab : unit -> Pp.std_ppcmds i*) -(* For translator *) +(** For translator *) val process_module_bindings : module_ident list -> (mod_bound_id * (module_struct_entry * bool)) list -> unit diff --git a/library/decls.mli b/library/decls.mli index 29fa13ae5..091ec7d99 100644 --- a/library/decls.mli +++ b/library/decls.mli @@ -1,10 +1,10 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* variable_data -> unit val variable_path : variable -> dir_path diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli index f9d0f9b4f..bc9541cf4 100644 --- a/library/dischargedhypsmap.mli +++ b/library/dischargedhypsmap.mli @@ -1,24 +1,23 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* discharged_hyps -> unit val get_discharged_hyps : full_path -> discharged_hyps diff --git a/library/global.mli b/library/global.mli index a8d76c4f4..17ad57138 100644 --- a/library/global.mli +++ b/library/global.mli @@ -1,14 +1,13 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Sign.named_context val env_is_empty : unit -> bool -(*s Extending env with variables and local definitions *) +(** {6 Extending env with variables and local definitions } *) val push_named_assum : (identifier * types) -> Univ.constraints val push_named_def : (identifier * constr * types option) -> Univ.constraints -(*s Adding constants, inductives, modules and module types. All these +(** {6 Sect } *) +(** Adding constants, inductives, modules and module types. All these functions verify that given names match those generated by kernel *) val add_constant : @@ -61,11 +61,11 @@ val add_constraints : constraints -> unit val set_engagement : engagement -> unit -(*s Interactive modules and module types *) -(* Both [start_*] functions take the [dir_path] argument to create a +(** {6 Interactive modules and module types } + Both [start_*] functions take the [dir_path] argument to create a [mod_self_id]. This should be the name of the compilation unit. *) -(* [start_*] functions return the [module_path] valid for components +(** [start_*] functions return the [module_path] valid for components of the started module / module type *) val start_module : identifier -> module_path @@ -81,7 +81,7 @@ val end_modtype : Summary.frozen -> identifier -> module_path val pack_module : unit -> module_body -(* Queries *) +(** Queries *) val lookup_named : variable -> named_declaration val lookup_constant : constant -> constant_body val lookup_inductive : inductive -> mutual_inductive_body * one_inductive_body @@ -91,17 +91,18 @@ val lookup_modtype : module_path -> module_type_body val constant_of_delta : constant -> constant val mind_of_delta : mutual_inductive -> mutual_inductive -(* Compiled modules *) +(** Compiled modules *) val start_library : dir_path -> module_path val export : dir_path -> module_path * compiled_library val import : compiled_library -> Digest.t -> module_path -(*s Function to get an environment from the constants part of the global +(** {6 Sect } *) +(** Function to get an environment from the constants part of the global * environment and a given context. *) val type_of_global : Libnames.global_reference -> types val env_of_context : Environ.named_context_val -> Environ.env -(* spiwack: register/unregister function for retroknowledge *) +(** spiwack: register/unregister function for retroknowledge *) val register : Retroknowledge.field -> constr -> constr -> unit diff --git a/library/goptions.mli b/library/goptions.mli index 511986a57..a8ed8a045 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -1,16 +1,16 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 'a -(*s Tables. *) +(** {6 Tables. } *) -(* The functor [MakeStringTable] declares a table containing objects +(** The functor [MakeStringTable] declares a table containing objects of type [string]; the function [member_message] say what to print when invoking the "Test Toto Titi foo." command; at the end [title] is the table name printed when invoking the "Print Toto Titi." @@ -85,7 +83,7 @@ sig val elements : unit -> string list end -(* The functor [MakeRefTable] declares a new table of objects of type +(** The functor [MakeRefTable] declares a new table of objects of type [A.t] practically denoted by [reference]; the encoding function [encode : reference -> A.t] is typically a globalization function, possibly with some restriction checks; the function @@ -113,9 +111,9 @@ module MakeRefTable : end -(*s Options. *) +(** {6 Options. } *) -(* These types and function are for declaring a new option of name [key] +(** These types and function are for declaring a new option of name [key] and access functions [read] and [write]; the parameter [name] is the option name used when printing the option value (command "Print Toto Titi." *) @@ -127,7 +125,7 @@ type 'a option_sig = { optwrite : 'a -> unit } -(* When an option is declared synchronous ([optsync] is [true]), the output is +(** When an option is declared synchronous ([optsync] is [true]), the output is a synchronous write function. Otherwise it is [optwrite] *) type 'a write_function = 'a -> unit @@ -137,7 +135,7 @@ val declare_bool_option : bool option_sig -> bool write_function val declare_string_option: string option_sig -> string write_function -(*s Special functions supposed to be used only in vernacentries.ml *) +(** {6 Special functions supposed to be used only in vernacentries.ml } *) val get_string_table : option_name -> @@ -153,7 +151,7 @@ val get_ref_table : mem : reference -> unit; print : unit > -(* The first argument is a locality flag. [Some true] = "Local", [Some false]="Global". *) +(** The first argument is a locality flag. [Some true] = "Local", [Some false]="Global". *) val set_int_option_value_gen : bool option -> option_name -> int option -> unit val set_bool_option_value_gen : bool option -> option_name -> bool -> unit val set_string_option_value_gen : bool option -> option_name -> string -> unit diff --git a/library/heads.mli b/library/heads.mli index 203da612f..bddee835f 100644 --- a/library/heads.mli +++ b/library/heads.mli @@ -1,12 +1,12 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit -(* [is_rigid] tells if some term is known to ultimately reduce to a term +(** [is_rigid] tells if some term is known to ultimately reduce to a term with a rigid head symbol *) val is_rigid : env -> constr -> bool diff --git a/library/impargs.mli b/library/impargs.mli index e8191e863..dc66e5493 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -1,22 +1,21 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit @@ -36,7 +35,8 @@ val is_maximal_implicit_args : unit -> bool type implicits_flags val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b -(*s An [implicits_list] is a list of positions telling which arguments +(** {6 Sect } *) +(** An [implicits_list] is a list of positions telling which arguments of a reference can be automatically infered *) @@ -61,11 +61,11 @@ val force_inference_of : implicit_status -> bool val positions_of_implicits : implicits_list -> int list -(* Computation of the positions of arguments automatically inferable +(** Computation of the positions of arguments automatically inferable for an object of the given type in the given env *) val compute_implicits : env -> types -> implicits_list -(* A [manual_explicitation] is a tuple of a positional or named explicitation with +(** A [manual_explicitation] is a tuple of a positional or named explicitation with maximal insertion, force inference and force usage flags. Forcing usage makes the argument implicit even if the automatic inference considers it not inferable. *) type manual_explicitation = Topconstr.explicitation * (bool * bool * bool) @@ -73,7 +73,7 @@ type manual_explicitation = Topconstr.explicitation * (bool * bool * bool) val compute_implicits_with_manual : env -> types -> bool -> manual_explicitation list -> implicits_list -(*s Computation of implicits (done using the global environment). *) +(** {6 Computation of implicits (done using the global environment). } *) val declare_var_implicits : variable -> unit val declare_constant_implicits : constant -> unit @@ -81,7 +81,7 @@ val declare_mib_implicits : mutual_inductive -> unit val declare_implicits : bool -> global_reference -> unit -(* [declare_manual_implicits local ref enriching l] +(** [declare_manual_implicits local ref enriching l] Manual declaration of which arguments are expected implicit. If not set, we decide if it should enrich by automatically inferd implicits depending on the current state. @@ -90,7 +90,7 @@ val declare_implicits : bool -> global_reference -> unit val declare_manual_implicits : bool -> global_reference -> ?enriching:bool -> manual_explicitation list -> unit -(* If the list is empty, do nothing, otherwise declare the implicits. *) +(** If the list is empty, do nothing, otherwise declare the implicits. *) val maybe_declare_manual_implicits : bool -> global_reference -> ?enriching:bool -> manual_explicitation list -> unit diff --git a/library/lib.mli b/library/lib.mli index 13c9baf65..e8b905f26 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -1,15 +1,16 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Libnames.object_prefix -> lib_objects -> unit val load_objects : int -> Libnames.object_prefix -> lib_objects -> unit val subst_objects : Mod_subst.substitution -> lib_objects -> lib_objects (*val load_and_subst_objects : int -> Libnames.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects*) -(* [classify_segment seg] verifies that there are no OpenedThings, +(** [classify_segment seg] verifies that there are no OpenedThings, clears ClosedSections and FrozenStates and divides Leafs according to their answers to the [classify_object] function in three groups: [Substitute], [Keep], [Anticipate] respectively. The order of each @@ -43,41 +44,45 @@ val subst_objects : Mod_subst.substitution -> lib_objects -> lib_objects val classify_segment : library_segment -> lib_objects * lib_objects * Libobject.obj list -(* [segment_of_objects prefix objs] forms a list of Leafs *) +(** [segment_of_objects prefix objs] forms a list of Leafs *) val segment_of_objects : Libnames.object_prefix -> lib_objects -> library_segment -(*s Adding operations (which call the [cache] method, and getting the +(** {6 Sect } *) +(** Adding operations (which call the [cache] method, and getting the current list of operations (most recent ones coming first). *) val add_leaf : Names.identifier -> Libobject.obj -> Libnames.object_name val add_anonymous_leaf : Libobject.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 : Names.identifier -> Libobject.obj list -> Libnames.object_name val add_frozen_state : unit -> unit -(* Adds a "dummy" entry in lib_stk with a unique new label number. *) +(** Adds a "dummy" entry in lib_stk with a unique new label number. *) val mark_end_of_command : unit -> unit -(* Returns the current label number *) + +(** Returns the current label number *) val current_command_label : unit -> int -(* [reset_label n ] resets [lib_stk] to the label n registered by + +(** [reset_label n ] resets [lib_stk] to the label n registered by [mark_end_of_command()]. That is it forgets the label and anything registered after it. *) val reset_label : int -> unit -(*s The function [contents_after] returns the current library segment, +(** {6 Sect } *) +(** The function [contents_after] returns the current library segment, starting from a given section path. If not given, the entire segment is returned. *) val contents_after : Libnames.object_name option -> library_segment -(*s Functions relative to current path *) +(** {6 Functions relative to current path } *) -(* User-side names *) +(** User-side names *) val cwd : unit -> Names.dir_path val cwd_except_section : unit -> Names.dir_path val current_dirpath : bool -> Names.dir_path (* false = except sections *) @@ -85,24 +90,24 @@ val make_path : Names.identifier -> Libnames.full_path val make_path_except_section : Names.identifier -> Libnames.full_path val path_of_include : unit -> Libnames.full_path -(* Kernel-side names *) +(** Kernel-side names *) val current_prefix : unit -> Names.module_path * Names.dir_path val make_kn : Names.identifier -> Names.kernel_name val make_con : Names.identifier -> Names.constant -(* Are we inside an opened section *) +(** Are we inside an opened section *) val sections_are_opened : unit -> bool val sections_depth : unit -> int -(* Are we inside an opened module type *) +(** Are we inside an opened module type *) val is_modtype : unit -> bool val is_module : unit -> bool val current_mod_id : unit -> Names.module_ident -(* Returns the opening node of a given name *) +(** Returns the opening node of a given name *) val find_opening_node : Names.identifier -> node -(*s Modules and module types *) +(** {6 Modules and module types } *) val start_module : bool option -> Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix @@ -113,30 +118,31 @@ val start_modtype : Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix val end_modtype : unit -> Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment -(* [Lib.add_frozen_state] must be called after each of the above functions *) -(*s Compilation units *) +(** [Lib.add_frozen_state] must be called after each of the above functions *) + +(** {6 Compilation units } *) val start_compilation : Names.dir_path -> Names.module_path -> unit val end_compilation : Names.dir_path -> Libnames.object_prefix * library_segment -(* The function [library_dp] returns the [dir_path] of the current +(** The function [library_dp] returns the [dir_path] of the current compiling library (or [default_library]) *) val library_dp : unit -> Names.dir_path -(* Extract the library part of a name even if in a section *) +(** Extract the library part of a name even if in a section *) val dp_of_mp : Names.module_path -> Names.dir_path val split_mp : Names.module_path -> Names.dir_path * Names.dir_path val split_modpath : Names.module_path -> Names.dir_path * Names.identifier list val library_part : Libnames.global_reference -> Names.dir_path val remove_section_part : Libnames.global_reference -> Names.dir_path -(*s Sections *) +(** {6 Sections } *) val open_section : Names.identifier -> unit val close_section : unit -> unit -(*s Backtracking (undo). *) +(** {6 Backtracking (undo). } *) val reset_to : Libnames.object_name -> unit val reset_name : Names.identifier Util.located -> unit @@ -146,11 +152,11 @@ val reset_to_state : Libnames.object_name -> unit val has_top_frozen_state : unit -> Libnames.object_name option -(* [back n] resets to the place corresponding to the $n$-th call of +(** [back n] resets to the place corresponding to the {% $ %}n{% $ %}-th call of [mark_end_of_command] (counting backwards) *) val back : int -> unit -(*s We can get and set the state of the operations (used in [States]). *) +(** {6 We can get and set the state of the operations (used in [States]). } *) type frozen @@ -163,13 +169,13 @@ val declare_initial_state : unit -> unit val reset_initial : unit -> unit -(* XML output hooks *) +(** XML output hooks *) val set_xml_open_section : (Names.identifier -> unit) -> unit val set_xml_close_section : (Names.identifier -> unit) -> unit type binding_kind = Explicit | Implicit -(*s Section management for discharge *) +(** {6 Section management for discharge } *) type variable_info = Names.identifier * binding_kind * Term.constr option * Term.types type variable_context = variable_info list @@ -189,7 +195,7 @@ val add_section_kn : Names.mutual_inductive -> Sign.named_context -> unit val replacement_context : unit -> (Names.identifier array Names.Cmap.t * Names.identifier array Names.Mindmap.t) -(*s Discharge: decrease the section level if in the current section *) +(** {6 Discharge: decrease the section level if in the current section } *) val discharge_kn : Names.mutual_inductive -> Names.mutual_inductive val discharge_con : Names.constant -> Names.constant 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 *) diff --git a/library/libobject.mli b/library/libobject.mli index 9c0abafde..8b21971aa 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -1,20 +1,18 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 'a option; rebuild_function : 'a -> 'a } -(* The default object is a "Keep" object with empty methods. +(** The default object is a "Keep" object with empty methods. Object creators are advised to use the construction [{(default_object "MY_OBJECT") with cache_function = ... @@ -85,10 +83,11 @@ type 'a object_declaration = { val default_object : string -> 'a object_declaration -(* the identity substitution function *) +(** the identity substitution function *) val ident_subst_function : substitution * 'a -> 'a -(*s Given an object declaration, the function [declare_object] +(** {6 Sect } *) +(** Given an object declaration, the function [declare_object] will hand back two functions, the "injection" and "projection" functions for dynamically typed library-objects. *) diff --git a/library/library.mli b/library/library.mli index c6bd8fe0b..05b213350 100644 --- a/library/library.mli +++ b/library/library.mli @@ -1,21 +1,20 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* bool option -> unit val require_library_from_dirpath : (dir_path * string) list -> bool option -> unit val require_library_from_file : identifier option -> System.physical_path -> bool option -> unit -(*s Open a module (or a library); if the boolean is true then it's also +(** {6 Sect } *) +(** Open a module (or a library); if the boolean is true then it's also an export otherwise just a simple import *) val import_module : bool -> qualid located -> unit -(*s Start the compilation of a library *) +(** {6 Start the compilation of a library } *) val start_library : string -> dir_path * string -(*s End the compilation of a library and save it to a ".vo" file *) +(** {6 End the compilation of a library and save it to a ".vo" file } *) val save_library_to : dir_path -> string -> unit -(*s Interrogate the status of libraries *) +(** {6 Interrogate the status of libraries } *) - (* - Tell if a library is loaded or opened *) + (** - Tell if a library is loaded or opened *) val library_is_loaded : dir_path -> bool val library_is_opened : dir_path -> bool - (* - Tell which libraries are loaded or imported *) + (** - Tell which libraries are loaded or imported *) val loaded_libraries : unit -> dir_path list val opened_libraries : unit -> dir_path list - (* - Return the full filename of a loaded library. *) + (** - Return the full filename of a loaded library. *) val library_full_filename : dir_path -> string - (* - Overwrite the filename of all libraries (used when restoring a state) *) + (** - Overwrite the filename of all libraries (used when restoring a state) *) val overwrite_library_filenames : string -> unit -(*s Hook for the xml exportation of libraries *) +(** {6 Hook for the xml exportation of libraries } *) val set_xml_require : (dir_path -> unit) -> unit -(*s Global load paths: a load path is a physical path in the file +(** {6 Sect } *) +(** Global load paths: a load path is a physical path in the file system; to each load path is associated a Coq [dir_path] (the "logical" path of the physical path) *) @@ -70,7 +72,7 @@ val remove_load_path : System.physical_path -> unit val find_logical_path : System.physical_path -> dir_path val is_in_load_paths : System.physical_path -> bool -(*s Locate a library in the load paths *) +(** {6 Locate a library in the load paths } *) exception LibUnmappedDir exception LibNotFound type library_location = LibLoaded | LibInPath @@ -79,5 +81,5 @@ val locate_qualified_library : bool -> qualid -> library_location * dir_path * System.physical_path val try_locate_qualified_library : qualid located -> dir_path * string -(*s Statistics: display the memory use of a library. *) +(** {6 Statistics: display the memory use of a library. } *) val mem : dir_path -> Pp.std_ppcmds diff --git a/library/nameops.mli b/library/nameops.mli index f69bf3ff0..414ee94ad 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -1,24 +1,24 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Pp.std_ppcmds val pr_name : name -> Pp.std_ppcmds 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 atompart_of_id : identifier -> string (** remove trailing digits *) +val root_of_id : identifier -> identifier (** remove trailing digits, {% $ %}'{% $ %} and {% $ %}\_{% $ %} *) val add_suffix : identifier -> string -> identifier val add_prefix : string -> identifier -> identifier @@ -38,17 +38,17 @@ val name_fold_map : ('a -> identifier -> 'a * identifier) -> 'a -> name -> 'a * val pr_lab : label -> Pp.std_ppcmds -(* some preset paths *) +(** some preset paths *) val default_library : dir_path -(* This is the root of the standard library of Coq *) +(** This is the root of the standard library of Coq *) val coq_root : module_ident -(* This is the default root prefix for developments which doesn't +(** This is the default root prefix for developments which doesn't mention a root *) val default_root_prefix : dir_path -(* Metavariables *) +(** Metavariables *) val pr_meta : Term.metavariable -> Pp.std_ppcmds val string_of_meta : Term.metavariable -> string diff --git a/library/nametab.mli b/library/nametab.mli index 98a482896..749d00343 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -1,21 +1,20 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* full_user_name -> object_reference -> unit] Registers the [object_reference] to be referred to by the @@ -58,29 +57,29 @@ open Libnames 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} + {% \end{%}itemize{% }%} *) exception GlobalizationError of qualid exception GlobalizationConstantError of qualid -(* Raises a globalization error *) +(** Raises a globalization error *) val error_global_not_found_loc : loc -> qualid -> 'a val error_global_not_found : qualid -> 'a val error_global_constant_not_found_loc : loc -> qualid -> 'a -(*s Register visibility of things *) +(** {6 Register visibility of things } *) -(* The visibility can be registered either - \begin{itemize} +(** The visibility can be registered either + {% \begin{%}itemize{% }%} \item for all suffixes not shorter then a given int -- when the object is loaded inside a module -- or \item for a precise suffix, when the module containing (the module containing ...) the object is opened (imported) - \end{itemize} + {% \end{%}itemize{% }%} *) type visibility = Until of int | Exactly of int @@ -94,9 +93,9 @@ type ltac_constant = kernel_name val push_tactic : visibility -> full_path -> ltac_constant -> unit -(*s The following functions perform globalization of qualified names *) +(** {6 The following functions perform globalization of qualified names } *) -(* These functions globalize a (partially) qualified name or fail with +(** These functions globalize a (partially) qualified name or fail with [Not_found] *) val locate : qualid -> global_reference @@ -109,59 +108,60 @@ val locate_module : qualid -> module_path val locate_section : qualid -> dir_path val locate_tactic : qualid -> ltac_constant -(* These functions globalize user-level references into global +(** These functions globalize user-level references into global references, like [locate] and co, but raise a nice error message in case of failure *) val global : reference -> global_reference val global_inductive : reference -> inductive -(* These functions locate all global references with a given suffix; +(** These functions locate all global references with a given suffix; if [qualid] is valid as such, it comes first in the list *) val locate_all : qualid -> global_reference list val locate_extended_all : qualid -> extended_global_reference list -(* Mapping a full path to a global reference *) +(** Mapping a full path to a global reference *) val global_of_path : full_path -> global_reference val extended_global_of_path : full_path -> extended_global_reference -(*s These functions tell if the given absolute name is already taken *) +(** {6 These functions tell if the given absolute name is already taken } *) val exists_cci : full_path -> bool val exists_modtype : full_path -> bool val exists_dir : dir_path -> bool -val exists_section : dir_path -> bool (* deprecated synonym of [exists_dir] *) -val exists_module : dir_path -> bool (* deprecated synonym of [exists_dir] *) +val exists_section : dir_path -> bool (** deprecated synonym of [exists_dir] *) +val exists_module : dir_path -> bool (** deprecated synonym of [exists_dir] *) -(*s These functions locate qualids into full user names *) +(** {6 These functions locate qualids into full user names } *) val full_name_cci : qualid -> full_path val full_name_modtype : qualid -> full_path val full_name_module : qualid -> dir_path -(*s Reverse lookup -- finding user names corresponding to the given +(** {6 Sect } *) +(** Reverse lookup -- finding user names corresponding to the given internal name *) -(* Returns the full path bound to a global reference or syntactic +(** Returns the full path bound to a global reference or syntactic definition, and the (full) dirpath associated to a module path *) val path_of_syndef : syndef_name -> full_path val path_of_global : global_reference -> full_path val dirpath_of_module : module_path -> dir_path -(* Returns in particular the dirpath or the basename of the full path +(** Returns in particular the dirpath or the basename of the full path associated to global reference *) val dirpath_of_global : global_reference -> dir_path val basename_of_global : global_reference -> identifier -(* Printing of global references using names as short as possible *) +(** Printing of global references using names as short as possible *) 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. *) @@ -171,7 +171,7 @@ val shortest_qualid_of_modtype : module_path -> qualid val shortest_qualid_of_module : module_path -> qualid val shortest_qualid_of_tactic : ltac_constant -> qualid -(* Deprecated synonyms *) +(** Deprecated synonyms *) val extended_locate : qualid -> extended_global_reference (*= locate_extended *) -val absolute_reference : full_path -> global_reference (* = global_of_path *) +val absolute_reference : full_path -> global_reference (** = global_of_path *) diff --git a/library/states.mli b/library/states.mli index 782e41ca7..fb11756e5 100644 --- a/library/states.mli +++ b/library/states.mli @@ -1,14 +1,15 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* state val unfreeze : state -> unit -(*s Rollback. [with_heavy_rollback f x] applies [f] to [x] and restores the +(** {6 Sect } *) +(** Rollback. [with_heavy_rollback f x] applies [f] to [x] and restores the state of the whole system as it was before the evaluation if an exception is raised. *) val with_heavy_rollback : ('a -> 'b) -> 'a -> 'b -(*s [with_state_protection f x] applies [f] to [x] and restores the +(** {6 Sect } *) +(** [with_state_protection f x] applies [f] to [x] and restores the state of the whole system as it was before the evaluation of f *) val with_state_protection : ('a -> 'b) -> 'a -> 'b diff --git a/library/summary.mli b/library/summary.mli index e6e17ef8c..58272aadb 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -1,14 +1,14 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(*