From 89aefbacd26b5febe36274f722e67d25f6d42aeb Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 26 Mar 2020 14:50:56 +0100
Subject: Shrink refman-prelude files.

---
 doc/sphinx/addendum/program.rst | 14 +++++++-------
 doc/sphinx/addendum/ring.rst    |  4 ++++
 2 files changed, 11 insertions(+), 7 deletions(-)

(limited to 'doc/sphinx/addendum')

diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index cbb5c0db8a..5cffe9e435 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -162,7 +162,7 @@ Program Definition
 
    This command types the value term in Russell and generates proof
    obligations. Once solved using the commands shown below, it binds the
-   final |Coq| term to the name ``ident`` in the environment.
+   final |Coq| term to the name :n:`@ident` in the environment.
 
    .. exn:: @ident already exists.
       :name: @ident already exists. (Program Definition)
@@ -170,12 +170,12 @@ Program Definition
 
    .. cmdv:: Program Definition @ident : @type := @term
 
-      It interprets the type ``type``, potentially generating proof
+      It interprets the type :n:`@type`, potentially generating proof
       obligations to be resolved. Once done with them, we have a |Coq|
-      type |type_0|. It then elaborates the preterm ``term`` into a |Coq|
-      term |term_0|, checking that the type of |term_0| is coercible to
-      |type_0|, and registers ``ident`` as being of type |type_0| once the
-      set of obligations generated during the interpretation of |term_0|
+      type :n:`@type__0`. It then elaborates the preterm :n:`@term` into a |Coq|
+      term :n:`@term__0`, checking that the type of :n:`@term__0` is coercible to
+      :n:`@type__0`, and registers :n:`@ident` as being of type :n:`@type__0` once the
+      set of obligations generated during the interpretation of :n:`@term__0`
       and the aforementioned coercion derivation are solved.
 
       .. exn:: In environment … the term: @term does not have type @type. Actually, it has type ...
@@ -185,7 +185,7 @@ Program Definition
 
       This is equivalent to:
 
-      :g:`Program Definition ident : forall binders, type := fun binders => term`.
+      :n:`Program Definition @ident : forall {* @binder }, @type := fun {* @binder } => @term`.
 
       .. TODO refer to production in alias
 
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index 76174e32b5..2a321b5cbf 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -1,8 +1,12 @@
+.. |bdi| replace:: :math:`\beta\delta\iota`
 .. |ra| replace:: :math:`\rightarrow_{\beta\delta\iota}`
 .. |la| replace:: :math:`\leftarrow_{\beta\delta\iota}`
 .. |eq| replace:: `=`:sub:`(by the main correctness theorem)`
 .. |re| replace:: ``(PEeval`` `v` `ap`\ ``)``
 .. |le| replace:: ``(Pphi_dev`` `v` ``(norm`` `ap`\ ``))``
+.. |N| replace:: ``N``
+.. |nat| replace:: ``nat``
+.. |Z| replace:: ``Z``
 
 .. _theringandfieldtacticfamilies:
 
-- 
cgit v1.2.3