From e367f1113738b28c42de6c87b7c9f3d0fce3f5be Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 20 Nov 2018 19:35:22 +0100
Subject: [sphinx] Progress towards closing #7602: remove most objects without
 a body.

Remove objects without body from most chapters.
The remaining problems are all in the SSReflect chapter.
---
 doc/sphinx/addendum/program.rst | 25 +++++++++++++------------
 1 file changed, 13 insertions(+), 12 deletions(-)

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

diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index fad45995d2..cc8870e2e4 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -150,6 +150,7 @@ Program Definition
 
    .. exn:: @ident already exists.
       :name: @ident already exists. (Program Definition)
+      :undocumented:
 
    .. cmdv:: Program Definition @ident : @type := @term
 
@@ -162,7 +163,7 @@ Program Definition
       and the aforementioned coercion derivation are solved.
 
       .. exn:: In environment … the term: @term does not have type @type. Actually, it has type ...
-
+         :undocumented:
 
    .. cmdv:: Program Definition @ident @binders : @type := @term
 
@@ -181,21 +182,21 @@ Program Fixpoint
 
 .. cmd:: Program Fixpoint @ident @params {? {@order}} : @type := @term
 
-The optional order annotation follows the grammar:
+   The optional order annotation follows the grammar:
 
-.. productionlist:: orderannot
-   order      : measure `term` (`term`)? | wf `term` `term`
+   .. productionlist:: orderannot
+      order      : measure `term` (`term`)? | wf `term` `term`
 
-+ :g:`measure f ( R )` where :g:`f` is a value of type :g:`X` computed on
-  any subset of the arguments and the optional (parenthesised) term
-  ``(R)`` is a relation on ``X``. By default ``X`` defaults to ``nat`` and ``R``
-  to ``lt``.
+   + :g:`measure f ( R )` where :g:`f` is a value of type :g:`X` computed on
+     any subset of the arguments and the optional (parenthesised) term
+     ``(R)`` is a relation on ``X``. By default ``X`` defaults to ``nat`` and ``R``
+     to ``lt``.
 
-+ :g:`wf R x` which is equivalent to :g:`measure x (R)`.
+   + :g:`wf R x` which is equivalent to :g:`measure x (R)`.
 
-The structural fixpoint operator behaves just like the one of |Coq| (see
-:cmd:`Fixpoint`), except it may also generate obligations. It works
-with mutually recursive definitions too.
+   The structural fixpoint operator behaves just like the one of |Coq| (see
+   :cmd:`Fixpoint`), except it may also generate obligations. It works
+   with mutually recursive definitions too.
 
 .. coqtop:: reset in
 
-- 
cgit v1.2.3