From 43b2ddf9db407f6e5481974a626ac5c91d74910f Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Thu, 14 Feb 2019 16:39:12 +0000
Subject: [Manual] Document primitive integers

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

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 342425567e..6c0290321d 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1240,6 +1240,8 @@ Exposing constants to OCaml libraries
    information is used for instance to define the return type of the
    :g:`#int63_eq` primitive.
 
+   .. seealso:: :ref:`primitive-integers`
+
 Inlining hints for the fast reduction machines
 ----------------------------------------------------------------
 
-- 
cgit v1.2.3