[coqlib] Rebindable Coqlib namespace.

We refactor the `Coqlib` API to locate objects over a namespace
`module.object.property`.

This introduces the vernacular command `Register g as n` to expose the
Coq constant `g` under the name `n` (through the `register_ref`
function). The constant can then be dynamically located using the
`lib_ref` function.

Co-authored-by: Emilio Jesús Gallego Arias <e+git@x80.org>
Co-authored-by: Maxime Dénès <mail@maximedenes.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>

1 files changed, 15 insertions, 0 deletions

diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index be65ff7570..125c4c25a3 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1200,3 +1200,18 @@ scope of their effect. There are four kinds of commands:
   modifier extends the effect outside the module even when the command
   occurs in a section.  The :cmd:`Set` and :cmd:`Unset` commands belong to this
   category.
+
+.. _exposing-constants-to-ocaml-libraries:
+
+Exposing constants to OCaml libraries
+----------------------------------------------------------------
+
+.. cmd:: Register @qualid__1 as @qualid__2
+
+   This command exposes the constant :n:`@qualid__1` to OCaml libraries under
+   the name :n:`@qualid__2`.  This constant can then be dynamically located
+   calling :n:`Coqlib.lib_ref "@qualid__2"`; i.e., there is no need to known
+   where is the constant defined (file, module, library, etc.).
+
+   Due to its internal nature, this command is not for general use. It is meant
+   to appear only in standard libraries and in support libraries of plug-ins.