There is no command to print currently available modules.

[Villetaneuse]

Is your feature request related to a problem?

There are commands to list required files (Print Libraries.), available constants (Search), but as far as I know, there is none to print currently available modules (which should probably include the libraries).

Proposed solution

I propose, as an easy and (hopefully) not so controversial solution, to add:

• Print Modules (which should also probably display functors)
• Print Module Types (which should also probably display functor types)

Alternative solutions

Another possible solution would be to have something more elaborate like Search, e.g.

SearchModule "Nat". (* display all module whose name contains `Nat` *)

or, maybe

Search kind:module "Nat".
Search kind:module_type "Nat".

Additional context

No response