diff options
| author | Vincent Laporte | 2019-02-14 15:54:22 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-02-25 10:05:34 +0000 |
| commit | 4c48fcace7612e2f1eaf7ffa6e5265282dd0b549 (patch) | |
| tree | 9bae56ae270c3b9fa93a34d4f5a5b4162afbecd7 /doc | |
| parent | 70b2ba35cacbfb9b790dd26364da18a39881ee0e (diff) | |
[Manual] Document “Register Inline”
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 11 |
1 files changed, 11 insertions, 0 deletions
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. |