Missing file in commit 1fb883.

It would seem that I forgot to include the actual documentation in 1fb883. As a result, the reference manual didn't compile due to missing dependencies.

1 files changed, 59 insertions, 0 deletions

diff --git a/doc/refman/Misc.tex b/doc/refman/Misc.tex
new file mode 100644
index 0000000000..c852708957
--- /dev/null
+++ b/doc/refman/Misc.tex
@@ -0,0 +1,59 @@
+\achapter{\protect{Miscellaneous extensions}}
+
+\asection{Program derivation}
+
+Coq comes with an extension called {\tt Derive}, which supports
+program derivation. Typically in the style of Bird and Meertens. 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$ From \term$_1$ Upto \term$_2$ As \ident$_2$]
+       {\tt Derive \ident$_1$ From \term$_1$ Upto \term$_2$ As \ident$_2$\comindex{Derive}}
+
+This commands opens a new proof with two goals. The first one has, as
+conclusion, the type of $\term_1$, but is shelved (see
+Section~\ref{shelve}). The visible goal has type {\tt \term$_2$
+\term$_1$ ?x} where {\tt ?x} is the existential variable
+corresponding to the shelved goal.
+
+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$_1$
+  \term$_2$ \ident$_1$}, 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 Coq.Numbers.Natural.Peano.NPeano.
+
+Section P.
+
+Variables (n m k:nat).
+
+\end{coq_example*}
+\begin{coq_example}
+Derive p From ((k*n)+(k*m)) Upto eq As h.
+Proof.
+rewrite <- Mult.mult_plus_distr_l.
+reflexivity.
+\end{coq_example}
+\begin{coq_example*}
+Qed.
+
+End P.
+
+\end{coq_example*}
+\begin{coq_example}
+Print p.
+Check h.
+\end{coq_example}
+
+As $\term_2$ does not need to be a symmetric relation, the
+{\tt Derive} extension may also be used for program refinement.