package coq-core

  1. Overview
  2. Docs
On This Page
  1. Module types
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

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

val declare_modtype : Names.Id.t -> module_params_expr -> module_expr list -> module_expr list -> Names.ModPath.t
val start_modtype : Names.Id.t -> module_params_expr -> module_expr list -> Names.ModPath.t
val end_modtype : unit -> Names.ModPath.t

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.

val import_module : Libobject.open_filter -> export:Lib.export_flag -> Names.ModPath.t -> unit
val 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

val declare_include : module_expr 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