From f1fa3386a01f06884fe7f71796a558eae3bb3e00 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 28 Nov 2018 16:03:11 +0100
Subject: Add indexes for coercion / substructure symbol :>.

And a few more Sphinx fixes in passing.
---
 doc/sphinx/language/coq-library.rst | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc/sphinx/language')

diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index 85474a3e98..10650af1d1 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -97,8 +97,8 @@ Logic
 The basic library of |Coq| comes with the definitions of standard
 (intuitionistic) logical connectives (they are defined as inductive
 constructions). They are equipped with an appealing syntax enriching the
-subclass `form` of the syntactic class `term`. The syntax of `form`
-is shown below:
+subclass :token:`form` of the syntactic class :token:`term`. The syntax of
+:token:`form` is shown below:
 
 .. /!\ Please keep the blanks in the lines below, experimentally they produce
    a nice last column. Or even better, find a proper way to do this!
-- 
cgit v1.2.3