From a27d9d43a8e1c1a1629cc72c87e582c323b503c7 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Mon, 18 Feb 2019 13:55:09 +0000
Subject: [Manual] Document the “Primitive” command

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

diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 001bacc9ec..342425567e 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1250,3 +1250,17 @@ Inlining hints for the fast reduction machines
 
    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.
+
+Registering primitive operations
+--------------------------------
+
+.. cmd:: Primitive @ident__1 := #@ident__2.
+
+   Declares :n:`@ident__1` as the primitive operator :n:`#@ident__2`. When
+   running this command, the type of the primitive should be already known by
+   the kernel (this is achieved through this command for primitive types and
+   through the :cmd:`Register` command with the :g:`kernel` name-space for other
+   types).
+
+   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