Module#

Ltac2.Module

The name of a module or module type. It may be a functor. It may also be currently open.

  • since 9.2
val equal : t -> t -> bool

equal m1 m2 tests equality of module names.

  • since 9.2
val to_message : t -> message

to_message m prints a module name.

  • since 9.2
val is_modtype : Environ.env -> t -> bool

is_modtype env m returns true if m is a module type or module type functor.

  • since 9.2
val is_functor : Environ.env -> t -> bool

is_functor env m returns true if m is a module functor or module type functor.

  • since 9.2
val is_bound_module : t -> bool

is_bound_module m returns true for modules which are arguments of a currently open functor (false for submodules of bound modules).

  • since 9.2
val is_library : t -> bool

is_library m returns true for modules which are libraries (i.e., files).

  • since 9.2
val is_open : t -> bool

is_open m returns true if m refers to a currently open interactive module (or module type or functor).

  • since 9.2
val parent_module : t -> t option

parent_module m returns the parent module, i.e., A for A.B. Toplevel modules (libraries) and bound modules (functor arguments) return None.

  • since 9.2
val module_of_reference : reference -> t

module_of_reference ref returns the module of the reference.

  • raises Invalid_argument

    if ref is a VarRef.

  • since 9.2
val current_module : unit -> t

current_module () returns a reference to the current innermost open interactive module.

  • since 9.2
val loaded_libraries : unit -> t list

loaded_libraries () returns the list of loaded library modules.

  • since 9.2
module Field : sig ... end
val module_contents : t -> Field.t list option

module_contents m returns the contents of the given module (None on closed functors and module types). Inductives are represented only by the first inductive of each mutual block (and no constructors).

  • since 9.2