package coq
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=3cbfc1e1a72b16d4744f5b64ede59586071e31d9c11c811a0372060727bfd9c3
doc/coq-core.vernac/Declaremods/index.html
Module DeclaremodsSource
Modules
Rigid / flexible module signature
Which module inline annotations should we honor, either None or the ones whose level is less or equal to the given integer
Kinds of modules
declare_module id fargs typ exprs declares module id, from functor arguments fargs, with final type typ. exprs is usually of length 1 (Module definition with a concrete body), but it could also be empty ("Declare Module", with non-empty typ), or multiple (body of the shape M <+ N <+ ...).
val declare_module :
Names.Id.t ->
module_params ->
(Constrexpr.module_ast * inline) module_signature ->
(Constrexpr.module_ast * inline) list ->
Names.ModPath.tval start_module :
bool option ->
Names.Id.t ->
module_params ->
(Constrexpr.module_ast * inline) module_signature ->
Names.ModPath.tModule types
declare_modtype interp_modast id fargs typs exprs Similar to declare_module, except that the types could be multiple
val declare_modtype :
Names.Id.t ->
module_params ->
(Constrexpr.module_ast * inline) list ->
(Constrexpr.module_ast * inline) list ->
Names.ModPath.tval start_modtype :
Names.Id.t ->
module_params ->
(Constrexpr.module_ast * inline) list ->
Names.ModPath.tLibraries i.e. modules on disk
val register_library :
library_name ->
Safe_typing.compiled_library ->
library_objects ->
Safe_typing.vodigest ->
Univ.ContextSet.t ->
unitval end_library :
?except:Future.UUIDSet.t ->
output_native_objects:bool ->
library_name ->
Safe_typing.compiled_library * library_objects * Nativelib.native_libraryappend a function to be executed at end_library
import_module export mp imports the module mp. It modifies Nametab and performs the open_object function for every object of the module. Raises Not_found when mp is unknown or when mp corresponds to a functor. If export is true, the module is also opened every time the module containing it is.
Same as import_module but for multiple modules, and more optimized than iterating import_module.
Include
...
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).
For printing modules, process_module_binding adds names of bound module (and its components) to Nametab. It also loads objects associated to it. It may raise a Failure when the bound module hasn't an atomic type.