diff options
Diffstat (limited to 'library/global.mli')
| -rw-r--r-- | library/global.mli | 39 |
1 files changed, 20 insertions, 19 deletions
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 |