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/addendum/program.rst | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'doc/sphinx/addendum/program.rst')

diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index cc8870e2e4..e153c7cbe2 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -102,7 +102,7 @@ Syntactic control over equalities
 
 To give more control over the generation of equalities, the
 type checker will fall back directly to |Coq|’s usual typing of dependent
-pattern matching if a return or in clause is specified. Likewise, the
+pattern matching if a ``return`` or ``in`` clause is specified. Likewise, the
 if construct is not treated specially by |Program| so boolean tests in
 the code are not automatically reflected in the obligations. One can
 use the :g:`dec` combinator to get the correct hypotheses as in:
@@ -118,8 +118,9 @@ use the :g:`dec` combinator to get the correct hypotheses as in:
      else S (pred n).
 
 The :g:`let` tupling construct :g:`let (x1, ..., xn) := t in b` does not
-produce an equality, contrary to the let pattern construct :g:`let ’(x1,
-..., xn) := t in b`. Also, :g:`term :>` explicitly asks the system to
+produce an equality, contrary to the let pattern construct
+:g:`let '(x1,..., xn) := t in b`.
+Also, :g:`term :>` explicitly asks the system to
 coerce term to its support type. It can be useful in notations, for
 example:
 
-- 
cgit v1.2.3