Merge PR #7131: Sphinx doc chapter 30

5 files changed, 69 insertions, 66 deletions

diff --git a/Makefile.doc b/Makefile.doc
index 0b45b9cec..fc791ce1c 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -60,8 +60,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \
   RefMan-gal.v.tex \
   RefMan-oth.v.tex RefMan-ltac.v.tex \
   RefMan-pro.v.tex \
-  Universes.v.tex \
-  Misc.v.tex)
+  Universes.v.tex)
 
 REFMANTEXFILES:=$(addprefix doc/refman/, \
   headers.sty Reference-Manual.tex \
diff --git a/doc/refman/Misc.tex b/doc/refman/Misc.tex
deleted file mode 100644
index ab00fbfe3..000000000
--- a/doc/refman/Misc.tex
+++ /dev/null
@@ -1,63 +0,0 @@
-\achapter{\protect{Miscellaneous extensions}}
-%HEVEA\cutname{miscellaneous.html}
-
-\asection{Program derivation}
-
-Coq comes with an extension called {\tt Derive}, which supports
-program derivation. Typically in the style of Bird and Meertens or
-derivations of program refinements. To use the {\tt Derive} extension
-it must first be required with {\tt Require Coq.Derive.Derive}. When
-the extension is loaded, it provides the following command.
-
-\subsection[\tt Derive \ident$_1$ SuchThat \term{} As \ident$_2$]
-       {\tt Derive \ident$_1$ SuchThat \term{} As \ident$_2$\comindex{Derive}}
-
-The name $\ident_1$ can appear in \term. This command opens a new
-proof presenting the user with a goal for \term{} in which the name
-$\ident_1$ is bound to a existential variables {\tt ?x} (formally,
-there are other goals standing for the existential variables but they
-are shelved, as described in Section~\ref{shelve}).
-
-When the proof ends two constants are defined:
-\begin{itemize}
-\item The first one is name $\ident_1$ and is defined as the proof of
-  the shelved goal (which is also the value of {\tt ?x}). It is
-always transparent.
-\item The second one is name $\ident_2$. It has type {\tt \term}, and
-  its body is the proof of the initially visible goal. It is opaque if
-  the proof ends with {\tt Qed}, and transparent if the proof ends
-  with {\tt Defined}.
-\end{itemize}
-
-\Example
-\begin{coq_example*}
-Require Coq.derive.Derive.
-Require Import Coq.Numbers.Natural.Peano.NPeano.
-
-Section P.
-
-Variables (n m k:nat).
-
-\end{coq_example*}
-\begin{coq_example}
-Derive p SuchThat ((k*n)+(k*m) = p) As h.
-Proof.
-rewrite <- Nat.mul_add_distr_l.
-subst p.
-reflexivity.
-\end{coq_example}
-\begin{coq_example*}
-Qed.
-
-End P.
-
-\end{coq_example*}
-\begin{coq_example}
-Print p.
-Check h.
-\end{coq_example}
-
-Any property can be used as \term, not only an equation. In
-particular, it could be an order relation specifying some form of
-program refinement or a non-executable property from which deriving a
-program is convenient.
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 7e68dd752..e51116007 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -118,7 +118,6 @@ Options A and B of the licence are {\em not} elected.}
 \part{Addendum to the Reference Manual}
 \include{AddRefMan-pre}%
 \include{Universes.v}% Universe polymorphes
-\include{Misc.v}
 %BEGIN LATEX
 \RefManCutCommand{ENDADDENDUM=\thepage}
 %END LATEX
diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst
new file mode 100644
index 000000000..b0343a8f0
--- /dev/null
+++ b/doc/sphinx/addendum/miscellaneous-extensions.rst
@@ -0,0 +1,67 @@
+.. include:: ../replaces.rst
+
+.. _miscellaneousextensions:
+
+Miscellaneous extensions
+=======================
+
+:Source: https://coq.inria.fr/distrib/current/refman/miscellaneous.html
+:Converted by: Paul Steckler
+
+.. contents::
+   :local:
+   :depth: 1
+----
+
+Program derivation
+-----------------
+
+|Coq| comes with an extension called ``Derive``, which supports program
+derivation. Typically in the style of Bird and Meertens or derivations
+of program refinements. To use the Derive extension it must first be
+required with ``Require Coq.Derive.Derive``. When the extension is loaded,
+it provides the following command:
+
+.. cmd:: Derive @ident SuchThat @term As @ident
+
+The first `ident` can appear in `term`. This command opens a new proof
+presenting the user with a goal for term in which the name `ident` is
+bound to an existential variable `?x` (formally, there are other goals
+standing for the existential variables but they are shelved, as
+described in Section :ref:`TODO-8.17.4`).
+
+When the proof ends two constants are defined:
+
++ The first one is named using the first `ident` and is defined as the proof of the
+  shelved goal (which is also the value of `?x`). It is always
+  transparent.
++ The second one is named using the second `ident`. It has type `term`, and its body is
+  the proof of the initially visible goal. It is opaque if the proof
+  ends with ``Qed``, and transparent if the proof ends with ``Defined``.
+
+.. example::
+  .. coqtop:: all
+
+     Require Coq.derive.Derive.
+     Require Import Coq.Numbers.Natural.Peano.NPeano.
+
+     Section P.
+
+     Variables (n m k:nat).
+
+     Derive p SuchThat ((k*n)+(k*m) = p) As h.
+     Proof.
+     rewrite <- Nat.mul_add_distr_l.
+     subst p.
+     reflexivity.
+     Qed.
+
+     End P.
+
+     Print p.
+     Check h.
+
+Any property can be used as `term`, not only an equation. In particular,
+it could be an order relation specifying some form of program
+refinement or a non-executable property from which deriving a program
+is convenient.
diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst
index 3dd4f8020..db03693ff 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index.rst
@@ -55,6 +55,7 @@ Table of contents
    addendum/nsatz
    addendum/generalized-rewriting
    addendum/parallel-proof-processing
+   addendum/miscellaneous-extensions
 
 .. toctree::
    :caption: Reference