From d5bb8a4ae2f509532ecfb4a53bb91c64d992c2e6 Mon Sep 17 00:00:00 2001
From: Clément Pit-Claudel
Date: Fri, 4 May 2018 19:02:11 -0400
Subject: [doc] Address feedback on doc writer guide

Co-Authored-By: @Zimmi48
---
 doc/sphinx/addendum/implicit-coercions.rst | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

(limited to 'doc/sphinx/addendum')

diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index 152f4f6552..09faa06765 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -140,29 +140,29 @@ Declaration of Coercions
 
   .. warn:: Ambiguous path.
 
-    When the coercion `qualid` is added to the inheritance graph, non
-    valid coercion paths are ignored; they are signaled by a warning
-    displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`.
+     When the coercion :token:`qualid` is added to the inheritance graph, non
+     valid coercion paths are ignored; they are signaled by a warning
+     displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`.
 
   .. cmdv:: Local Coercion @qualid : @class >-> @class
 
-    Declares the construction denoted by `qualid` as a coercion local to
-    the current section.
+     Declares the construction denoted by `qualid` as a coercion local to
+     the current section.
 
   .. cmdv:: Coercion @ident := @term
 
-    This defines `ident` just like ``Definition`` `ident` ``:=`` `term`,
-    and then declares `ident` as a coercion between it source and its target.
+     This defines `ident` just like ``Definition`` `ident` ``:=`` `term`,
+     and then declares `ident` as a coercion between it source and its target.
 
   .. cmdv:: Coercion @ident := @term : @type
 
-    This defines `ident` just like ``Definition`` `ident` : `type` ``:=`` `term`,
-    and then declares `ident` as a coercion between it source and its target.
+     This defines `ident` just like ``Definition`` `ident` : `type` ``:=`` `term`,
+     and then declares `ident` as a coercion between it source and its target.
 
   .. cmdv:: Local Coercion @ident := @term
 
-    This defines `ident` just like ``Let`` `ident` ``:=`` `term`,
-    and then declares `ident` as a coercion between it source and its target.
+     This defines `ident` just like ``Let`` `ident` ``:=`` `term`,
+     and then declares `ident` as a coercion between it source and its target.
 
 Assumptions can be declared as coercions at declaration time.
 This extends the grammar of assumptions from
-- 
cgit v1.2.3