package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
Modules

Rigid / flexible module signature

type '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

type inline =
  1. | NoInline
  2. | DefaultInline
  3. | InlineAt of int

Kinds of modules

type module_params = (Names.lident list * (Constrexpr.module_ast * inline)) list
type module_params_expr = (Names.MBId.t list * module_expr) list
Libraries i.e. modules on disk
type library_name = Names.DirPath.t
type library_objects
module Synterp : sig ... end
module 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 <+ ...).

val start_library : library_name -> unit
val 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.

val iter_all_interp_segments : (Nametab.object_prefix -> Libobject.t -> unit) -> unit
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 objects associated to it. It may raise a Failure when the bound module hasn't an atomic type.

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

Compatibility layer

val import_module : Libobject.open_filter -> export:Lib.export_flag -> Names.ModPath.t -> unit
val end_module : unit -> Names.ModPath.t
val end_modtype : unit -> Names.ModPath.t
val declare_include : (Constrexpr.module_ast * inline) list -> unit
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct