Module `Declaremods`Source

Modules

Rigid / flexible module signature

Sourcetype 'a module_signature =

| Enforce of 'a
(*
... : T
*)
| Check of 'a list
(*
... <: T1 <: T2, possibly empty
*)

Which module inline annotations should we honor, either None or the ones whose level is less or equal to the given integer

Sourcetype inline =

| NoInline
| DefaultInline
| InlineAt of int

Kinds of modules

Source

type module_params =
  (Names.lident list * (Constrexpr.module_ast * inline)) list

Source

type module_expr =
  Modintern.module_struct_expr
  * Names.ModPath.t
  * Modintern.module_kind
  * Entries.inline

Sourcetype module_params_expr = (Names.MBId.t list * module_expr) list

Libraries i.e. modules on disk

Sourcetype library_name = Names.DirPath.t

Sourcetype library_objects

Sourcemodule Synterp : sig ... end

Sourcemodule Interp : sig ... end

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 <+ ...).

Sourceval start_library : library_name -> unit

Source

val end_library : 
  output_native_objects:bool ->
  library_name ->
  Safe_typing.compiled_library
  * library_objects
  * library_objects
  * Nativelib.native_library

Sourceval append_end_library_hook : (unit -> unit) -> unit

append a function to be executed at end_library

...

iter_all_interp_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). Ignores synterp objects.

Source

val iter_all_interp_segments : 
  (Nametab.object_prefix -> Libobject.t -> unit) ->
  unit

Sourceval 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 objects associated to it. It may raise a Failure when the bound module hasn't an atomic type.

Source

val process_module_binding : 
  Names.MBId.t ->
  (Constr.t * Univ.AbstractContext.t option) Declarations.module_alg_expr ->
  unit

Compatibility layer

Source

val import_module : 
  Libobject.open_filter ->
  export:Lib.export_flag ->
  Names.ModPath.t ->
  unit

Source

val declare_module : 
  Names.Id.t ->
  module_params ->
  (Constrexpr.module_ast * inline) module_signature ->
  (Constrexpr.module_ast * inline) list ->
  Names.ModPath.t

Source

val start_module : 
  Lib.export ->
  Names.Id.t ->
  module_params ->
  (Constrexpr.module_ast * inline) module_signature ->
  Names.ModPath.t

Sourceval end_module : unit -> Names.ModPath.t

Source

val declare_modtype : 
  Names.Id.t ->
  module_params ->
  (Constrexpr.module_ast * inline) list ->
  (Constrexpr.module_ast * inline) list ->
  Names.ModPath.t

Source

val start_modtype : 
  Names.Id.t ->
  module_params ->
  (Constrexpr.module_ast * inline) list ->
  Names.ModPath.t

Sourceval end_modtype : unit -> Names.ModPath.t

Sourceval declare_include : (Constrexpr.module_ast * inline) list -> unit

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.vernac/Declaremods/index.html

Module `Declaremods`Source

Modules

Libraries i.e. modules on disk

...

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.vernac/Declaremods/index.html

Module DeclaremodsSource

Modules

Libraries i.e. modules on disk

...

Module `Declaremods`Source