From 4c48fcace7612e2f1eaf7ffa6e5265282dd0b549 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Thu, 14 Feb 2019 15:54:22 +0000
Subject: [Manual] Document “Register Inline”

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

diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 1eacb95131..001bacc9ec 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1239,3 +1239,14 @@ Exposing constants to OCaml libraries
    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.
+
+Inlining hints for the fast reduction machines
+----------------------------------------------------------------
+
+.. cmd:: Register Inline @qualid
+
+   This command gives as a hint to the reduction machines (VM and native) that
+   the body of the constant :n:`@qualid` should be inlined in the generated code.
+
+   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.
-- 
cgit v1.2.3