package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.17.1.tar.gz
sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b

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

Module DeclaremodsSource

Modules

Rigid / flexible module signature

Sourcetype 'a module_signature =
  1. | Enforce of 'a
    (*

    ... : T

    *)
  2. | 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 =
  1. | NoInline
  2. | DefaultInline
  3. | InlineAt of int

Kinds of modules

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

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 end_module : unit -> Names.ModPath.t
Module types

declare_modtype interp_modast id fargs typs exprs Similar to declare_module, except that the types could be multiple

Sourceval end_modtype : unit -> Names.ModPath.t
Libraries i.e. modules on disk
Sourcetype library_name = Names.DirPath.t
Sourcetype library_objects
Sourceval start_library : library_name -> unit
Sourceval end_library : output_native_objects:bool -> library_name -> Safe_typing.compiled_library * library_objects * Nativelib.native_library
Sourceval append_end_library_hook : (unit -> unit) -> unit

append 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.

Sourceval import_module : Libobject.open_filter -> export:Lib.export_flag -> Names.ModPath.t -> unit
Sourceval import_modules : export:Lib.export_flag -> (Libobject.open_filter * Names.ModPath.t) list -> unit

Same as import_module but for multiple modules, and more optimized than iterating import_module.

Include

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

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

Sourceval iter_all_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.

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