Merge PR #186: [RFC] Coqlib cleanup

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.