diff options
Diffstat (limited to 'library/declaremods.mli')
| -rw-r--r-- | library/declaremods.mli | 42 |
1 files changed, 18 insertions, 24 deletions
diff --git a/library/declaremods.mli b/library/declaremods.mli index 3917fe8d..fd8d2961 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names @@ -13,10 +15,10 @@ open Vernacexpr type 'modast module_interpretor = Environ.env -> Misctypes.module_kind -> 'modast -> - Entries.module_struct_entry * Misctypes.module_kind + Entries.module_struct_entry * Misctypes.module_kind * Univ.ContextSet.t type 'modast module_params = - (Id.t Loc.located list * ('modast * inline)) list + (Misctypes.lident list * ('modast * inline)) list (** [declare_module interp_modast id fargs typ exprs] declares module [id], with structure constructed by [interp_modast] @@ -30,15 +32,15 @@ val declare_module : Id.t -> 'modast module_params -> ('modast * inline) module_signature -> - ('modast * inline) list -> module_path + ('modast * inline) list -> ModPath.t val start_module : 'modast module_interpretor -> bool option -> Id.t -> 'modast module_params -> - ('modast * inline) module_signature -> module_path + ('modast * inline) module_signature -> ModPath.t -val end_module : unit -> module_path +val end_module : unit -> ModPath.t @@ -53,23 +55,15 @@ val declare_modtype : 'modast module_params -> ('modast * inline) list -> ('modast * inline) list -> - module_path + ModPath.t val start_modtype : 'modast module_interpretor -> Id.t -> 'modast module_params -> - ('modast * inline) list -> module_path + ('modast * inline) list -> ModPath.t -val end_modtype : unit -> module_path - -(** Hooks for XML output *) -val xml_declare_module : (module_path -> unit) Hook.t -val xml_start_module : (module_path -> unit) Hook.t -val xml_end_module : (module_path -> unit) Hook.t -val xml_declare_module_type : (module_path -> unit) Hook.t -val xml_start_module_type : (module_path -> unit) Hook.t -val xml_end_module_type : (module_path -> unit) Hook.t +val end_modtype : unit -> ModPath.t (** {6 Libraries i.e. modules on disk } *) @@ -80,7 +74,7 @@ type library_objects val register_library : library_name -> Safe_typing.compiled_library -> library_objects -> Safe_typing.vodigest -> - Univ.universe_context_set -> unit + Univ.ContextSet.t -> unit val get_library_native_symbols : library_name -> Nativecode.symbols @@ -98,13 +92,13 @@ val append_end_library_hook : (unit -> unit) -> unit every object of the module. Raises [Not_found] when [mp] is unknown or when [mp] corresponds to a functor. *) -val really_import_module : module_path -> unit +val really_import_module : ModPath.t -> unit (** [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 +val import_module : bool -> ModPath.t -> unit (** Include *) @@ -121,7 +115,7 @@ val iter_all_segments : (Libnames.object_name -> Libobject.obj -> unit) -> unit -val debug_print_modtab : unit -> Pp.std_ppcmds +val debug_print_modtab : unit -> Pp.t (** For printing modules, [process_module_binding] adds names of bound module (and its components) to Nametab. It also loads |