From 70b2ba35cacbfb9b790dd26364da18a39881ee0e Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Thu, 14 Feb 2019 15:47:18 +0000
Subject: [Manual] Document “Register” to kernel namespace

---
 doc/sphinx/proof-engine/vernacular-commands.rst | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index a98a46ba21..1eacb95131 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1227,3 +1227,15 @@ Exposing constants to OCaml libraries
 
    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.
+
+   As a special case, when the first segment of :n:`@qualid__2` is :g:`kernel`,
+   the constant is exposed to the kernel. For instance, the `Int63` module
+   features the following declaration:
+
+   .. coqdoc::
+
+      Register bool as kernel.ind_bool.
+
+   This makes the kernel aware of what is the type of boolean values. This
+   information is used for instance to define the return type of the
+   :g:`#int63_eq` primitive.
-- 
cgit v1.2.3