From bbd53a978e1107f2840bad189b440007f4225795 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 22 Mar 2018 10:25:57 +0100
Subject: [Sphinx] Remove duplicate entry for command `Coercion`

---
 doc/sphinx/language/gallina-extensions.rst | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 68066faa30..1d6c11b38d 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -2191,12 +2191,7 @@ an inductive type or any constant with a type of the form
 Then the user is able to apply an object that is not a function, but
 can be coerced to a function, and more generally to consider that a
 term of type ``A`` is of type ``B`` provided that there is a declared coercion
-between ``A`` and ``B``. The main command is
-
-.. cmd:: Coercion @qualid : @class >-> @class.
-
-which declares the construction denoted by qualid as a coercion
-between the two given classes.
+between ``A`` and ``B``.
 
 More details and examples, and a description of the commands related
 to coercions are provided in :ref:`implicitcoercions`.
-- 
cgit v1.2.3