diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 15 |
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. |