diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/decl_kinds.mli | 38 | ||||
| -rw-r--r-- | library/declare.mli | 40 | ||||
| -rw-r--r-- | library/declaremods.mli | 44 | ||||
| -rw-r--r-- | library/decls.mli | 16 | ||||
| -rw-r--r-- | library/dischargedhypsmap.mli | 21 | ||||
| -rw-r--r-- | library/global.mli | 39 | ||||
| -rw-r--r-- | library/goptions.mli | 42 | ||||
| -rw-r--r-- | library/heads.mli | 20 | ||||
| -rw-r--r-- | library/impargs.mli | 32 | ||||
| -rw-r--r-- | library/lib.mli | 76 | ||||
| -rw-r--r-- | library/libnames.mli | 66 | ||||
| -rw-r--r-- | library/libobject.mli | 25 | ||||
| -rw-r--r-- | library/library.mli | 48 | ||||
| -rw-r--r-- | library/nameops.mli | 28 | ||||
| -rwxr-xr-x | library/nametab.mli | 68 | ||||
| -rw-r--r-- | library/states.mli | 23 | ||||
| -rw-r--r-- | library/summary.mli | 16 |
17 files changed, 325 insertions, 317 deletions
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 *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(*********************************************************************** + v * The Coq Proof Assistant / The Coq Development Team + <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud + \VV/ ************************************************************* + // * This file is distributed under the terms of the + * GNU Lesser General Public License Version 2.1 + ***********************************************************************) -(* $Id$ *) +(** {% $ %}Id: decl_kinds.mli 12337 2009-09-17 15:58:14Z glondu {% $ %} *) open Util open Libnames -(* Informal mathematical status of declarations *) +(** Informal mathematical status of declarations *) type locality = | Local @@ -44,7 +44,7 @@ type definition_object_kind = type assumption_object_kind = Definitional | Logical | Conjectural -(* [assumption_kind] +(** [assumption_kind] | Local | Global ------------------------------------ @@ -56,7 +56,7 @@ type assumption_kind = locality * assumption_object_kind type definition_kind = locality * boxed_flag * definition_object_kind -(* Kinds used in proofs *) +(** Kinds used in proofs *) type goal_object_kind = | DefinitionBody of definition_object_kind @@ -64,31 +64,31 @@ type goal_object_kind = type goal_kind = locality * goal_object_kind -(* Kinds used in library *) +(** Kinds used in library *) type logical_kind = | IsAssumption of assumption_object_kind | IsDefinition of definition_object_kind | IsProof of theorem_kind -(* Utils *) +(** Utils *) val logical_kind_of_goal_kind : goal_object_kind -> 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 *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(*********************************************************************** + v * The Coq Proof Assistant / The Coq Development Team + <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud + \VV/ ************************************************************* + // * This file is distributed under the terms of the + * GNU Lesser General Public License Version 2.1 + ***********************************************************************) (*i $Id$ i*) -(*i*) open Names open Libnames open Term @@ -19,9 +18,8 @@ open Indtypes open Safe_typing open Nametab open Decl_kinds -(*i*) -(* This module provides the official functions to declare new variables, +(** This module provides the official functions to declare new variables, parameters, constants and inductive types. Using the following functions will add the entries in the global environment (module [Global]), will register the declarations in the library (module [Lib]) --- so that the @@ -30,22 +28,22 @@ open Decl_kinds open Nametab -(* Declaration of local constructions (Variable/Hypothesis/Local) *) +(** Declaration of local constructions (Variable/Hypothesis/Local) *) type section_variable_entry = - | SectionLocalDef of constr * types option * bool (* opacity *) - | SectionLocalAssum of types * bool (* Implicit status *) + | SectionLocalDef of constr * types option * bool (** opacity *) + | SectionLocalAssum of types * bool (** Implicit status *) type variable_declaration = dir_path * section_variable_entry * logical_kind val declare_variable : variable -> 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 *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(*********************************************************************** + v * The Coq Proof Assistant / The Coq Development Team + <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud + \VV/ ************************************************************* + // * This file is distributed under the terms of the + * GNU Lesser General Public License Version 2.1 + ***********************************************************************) (*i $Id$ i*) -(*i*) open Util open Names open Entries @@ -16,15 +15,16 @@ open Environ open Libnames open Libobject open Lib - (*i*) + (**/**) -(*s This modules provides official functions to declare modules and +(** {6 Sect } *) +(** This modules provides official functions to declare modules and module types *) -(*s Modules *) +(** {6 Modules } *) -(* [declare_module interp_modtype interp_modexpr id fargs typ expr] +(** [declare_module interp_modtype interp_modexpr id fargs typ expr] declares module [id], with type constructed by [interp_modtype] from functor arguments [fargs] and [typ] and with module body constructed by [interp_modtype] from functor arguments [fargs] and @@ -53,7 +53,7 @@ val end_module : unit -> 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 *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(*********************************************************************** + v * The Coq Proof Assistant / The Coq Development Team + <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud + \VV/ ************************************************************* + // * This file is distributed under the terms of the + * GNU Lesser General Public License Version 2.1 + ***********************************************************************) (*i $Id$ i*) @@ -20,7 +20,7 @@ open Decl_kinds (** Registration and access to the table of variable *) type variable_data = - dir_path * bool (* opacity *) * Univ.constraints * logical_kind + dir_path * bool (** opacity *) * Univ.constraints * logical_kind val add_variable_data : variable -> 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 *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(*********************************************************************** + v * The Coq Proof Assistant / The Coq Development Team + <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud + \VV/ ************************************************************* + // * This file is distributed under the terms of the + * GNU Lesser General Public License Version 2.1 + ***********************************************************************) (*i $Id$ i*) -(*i*) open Libnames open Term open Environ open Nametab -(*i*) type discharged_hyps = full_path list -(*s Discharged hypothesis. Here we store the discharged hypothesis of each *) -(* constant or inductive type declaration. *) +(** {6 Sect } *) +(** Discharged hypothesis. Here we store the discharged hypothesis of each + constant or inductive type declaration. *) val set_discharged_hyps : full_path -> 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 *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(*********************************************************************** + v * The Coq Proof Assistant / The Coq Development Team + <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud + \VV/ ************************************************************* + // * This file is distributed under the terms of the + * GNU Lesser General Public License Version 2.1 + ***********************************************************************) (*i $Id$ i*) -(*i*) open Names open Univ open Term @@ -17,9 +16,9 @@ open Entries open Indtypes open Mod_subst open Safe_typing - (*i*) + (**/**) -(* This module defines the global environment of Coq. The functions +(** This module defines the global environment of Coq. The functions below are exactly the same as the ones in [Safe_typing], operating on that global environment. [add_*] functions perform name verification, i.e. check that the name given as argument match those provided by @@ -38,11 +37,12 @@ val named_context : unit -> 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 *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(*********************************************************************** + v * The Coq Proof Assistant / The Coq Development Team + <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud + \VV/ ************************************************************* + // * This file is distributed under the terms of the + * GNU Lesser General Public License Version 2.1 + ***********************************************************************) (*i $Id$ i*) -(* This module manages customization parameters at the vernacular level *) +(** This module manages customization parameters at the vernacular level *) -(* Two kinds of things are managed : tables and options value +(** Two kinds of things are managed : tables and options value - Tables are created by applying the [MakeTable] functor. - Variables storing options value are created by applying one of the [declare_int_option], [declare_bool_option], ... functions. @@ -40,12 +40,11 @@ Set Tata Tutu Titi. Unset Tata Tutu Titi. - Print Table Tata Tutu Titi. (* synonym: Test Table Tata Tutu Titi. *) + Print Table Tata Tutu Titi. (** synonym: Test Table Tata Tutu Titi. *) The created table/option may be declared synchronous or not (synchronous = consistent with the resetting commands) *) -(*i*) open Pp open Util open Names @@ -53,18 +52,17 @@ open Libnames open Term open Nametab open Mod_subst -(*i*) -(*s Things common to tables and options. *) +(** {6 Things common to tables and options. } *) -(* The type of table/option keys *) +(** The type of table/option keys *) type option_name = string list val error_undeclared_key : option_name -> '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 *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(*********************************************************************** + v * The Coq Proof Assistant / The Coq Development Team + <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud + \VV/ ************************************************************* + // * This file is distributed under the terms of the + * GNU Lesser General Public License Version 2.1 + ***********************************************************************) -(* $Id$ *) +(** {% $ %}Id: heads.mli 10841 2008-04-24 07:19:57Z herbelin {% $ %} *) open Names open Term @@ -17,12 +17,12 @@ open Environ provides the function to compute the head symbols and a table to store the heads *) -(* [declared_head] computes and registers the head symbol of a +(** [declared_head] computes and registers the head symbol of a possibly evaluable constant or variable *) val declare_head : evaluable_global_reference -> 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 *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(*********************************************************************** + v * The Coq Proof Assistant / The Coq Development Team + <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud + \VV/ ************************************************************* + // * This file is distributed under the terms of the + * GNU Lesser General Public License Version 2.1 + ***********************************************************************) (*i $Id$ i*) -(*i*) open Names open Libnames open Term open Environ open Nametab -(*i*) -(*s Implicit arguments. Here we store the implicit arguments. Notice that we +(** {6 Sect } *) +(** Implicit arguments. Here we store the implicit arguments. Notice that we are outside the kernel, which knows nothing about implicit arguments. *) val make_implicit_args : bool -> 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 *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(*********************************************************************** + v * The Coq Proof Assistant / The Coq Development Team + <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud + \VV/ ************************************************************* + // * This file is distributed under the terms of the + * GNU Lesser General Public License Version 2.1 + ***********************************************************************) (*i $Id$ i*) -(*s This module provides a general mechanism to keep a trace of all operations +(** {6 Sect } *) +(** This module provides a general mechanism to keep a trace of all operations and to backtrack (undo) those operations. It provides also the section mechanism (at a low level; discharge is not known at this step). *) @@ -28,14 +29,14 @@ and library_segment = (Libnames.object_name * node) list type lib_objects = (Names.identifier * Libobject.obj) list -(*s Object iteratation functions. *) +(** {6 Object iteratation functions. } *) val open_objects : int -> 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 *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(*********************************************************************** + v * The Coq Proof Assistant / The Coq Development Team + <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud + \VV/ ************************************************************* + // * This file is distributed under the terms of the + * GNU Lesser General Public License Version 2.1 + ***********************************************************************) (*i $Id$ i*) -(*i*) open Pp open Util open Names open Term open Mod_subst -(*i*) -(*s Global reference is a kernel side type for all references together *) +(** {6 Global reference is a kernel side type for all references together } *) type global_reference = | VarRef of variable | ConstRef of constant @@ -40,14 +38,14 @@ val destConstructRef : global_reference -> 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 *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(*********************************************************************** + v * The Coq Proof Assistant / The Coq Development Team + <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud + \VV/ ************************************************************* + // * This file is distributed under the terms of the + * GNU Lesser General Public License Version 2.1 + ***********************************************************************) (*i $Id$ i*) -(*i*) open Names open Libnames open Mod_subst -(*i*) -(* [Libobject] declares persistent objects, given with methods: +(** [Libobject] declares persistent objects, given with methods: * a caching function specifying how to add the object in the current scope; @@ -74,7 +72,7 @@ type 'a object_declaration = { discharge_function : object_name * 'a -> '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 *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(*********************************************************************** + v * The Coq Proof Assistant / The Coq Development Team + <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud + \VV/ ************************************************************* + // * This file is distributed under the terms of the + * GNU Lesser General Public License Version 2.1 + ***********************************************************************) (*i $Id$ i*) -(*i*) open Util open Names open Libnames open Libobject -(*i*) -(*s This module provides functions to load, open and save +(** {6 Sect } *) +(** This module provides functions to load, open and save libraries. Libraries correspond to the subclass of modules that coincide with a file on disk (the ".vo" files). Libraries on the disk comes with checksums (obtained with the [Digest] module), which @@ -23,43 +22,46 @@ open Libobject written at various dates. *) -(*s Require = load in the environment + open (if the optional boolean +(** {6 Sect } *) +(** Require = load in the environment + open (if the optional boolean is not [None]); mark also for export if the boolean is [Some true] *) val require_library : qualid located list -> 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 *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(*********************************************************************** + v * The Coq Proof Assistant / The Coq Development Team + <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud + \VV/ ************************************************************* + // * This file is distributed under the terms of the + * GNU Lesser General Public License Version 2.1 + ***********************************************************************) (*i $Id$ i*) open Names -(* Identifiers and names *) +(** Identifiers and names *) val pr_id : identifier -> 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 *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(*********************************************************************** + v * The Coq Proof Assistant / The Coq Development Team + <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud + \VV/ ************************************************************* + // * This file is distributed under the terms of the + * GNU Lesser General Public License Version 2.1 + ***********************************************************************) (*i $Id$ i*) -(*i*) open Util open Pp open Names open Libnames -(*i*) -(*s This module contains the tables for globalization, which +(** {6 Sect } *) +(** This module contains the tables for globalization, which associates internal object references to qualified names (qualid). There are three classes of names: @@ -32,8 +31,8 @@ open Libnames and [qualid] *) -(* Most functions in this module fall into one of the following categories: - \begin{itemize} +(** Most functions in this module fall into one of the following categories: + {% \begin{%}itemize{% }%} \item [push : visibility -> 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 *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(*********************************************************************** + v * The Coq Proof Assistant / The Coq Development Team + <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud + \VV/ ************************************************************* + // * This file is distributed under the terms of the + * GNU Lesser General Public License Version 2.1 + ***********************************************************************) (*i $Id$ i*) -(*s States of the system. In that module, we provide functions to get +(** {6 Sect } *) +(** States of the system. In that module, we provide functions to get and set the state of the whole system. Internally, it is done by freezing the states of both [Lib] and [Summary]. We provide functions to write and restore state to and from a given file. *) @@ -20,13 +21,15 @@ type state val freeze : unit -> 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 *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(*********************************************************************** + v * The Coq Proof Assistant / The Coq Development Team + <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud + \VV/ ************************************************************* + // * This file is distributed under the terms of the + * GNU Lesser General Public License Version 2.1 + ***********************************************************************) (*i $Id$ i*) -(* This module registers the declaration of global tables, which will be kept +(** This module registers the declaration of global tables, which will be kept in synchronization during the various backtracks of the system. *) type 'a summary_declaration = { |