A better Program documentation. Include it in the generated stdlib doc.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10061 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 5 deletions

diff --git a/doc/refman/AddRefMan-pre.tex b/doc/refman/AddRefMan-pre.tex
index 15776690ce..85811c1450 100644
--- a/doc/refman/AddRefMan-pre.tex
+++ b/doc/refman/AddRefMan-pre.tex
@@ -28,6 +28,11 @@ Manual.
   files from $\FW$ terms.   It is contributed by Jean-Christophe
   Filliâtre and Pierre Letouzey.
 
+\item[Program] This chapter explains the use of the \texttt{Program}
+  vernacular which allows the development of certified
+  programs in \Coq. It is contributed by Matthieu Sozeau and replaces
+  the previous \texttt{Program} tactic by Catherine Parent.
+
 %\item[Natural] This chapter is due to Yann Coscoy. It is the user
 %  manual of the tools he wrote for printing proofs in natural
 %  language. At this time, French and English languages are supported.
@@ -35,11 +40,6 @@ Manual.
 \item[omega] \texttt{omega}, written by Pierre Crégut, solves a whole
   class of arithmetic problems.
 
-%\item[Program] The \texttt{Program} technology intends to inverse the
-%  extraction mechanism. It allows the developments of certified
-%  programs in \Coq. This chapter is due to Catherine Parent. {\bf This
-%  feature is not available in {\Coq} version 7.}
-
 \item[The {\tt ring} tactic] This is a tactic to do AC rewriting. This
   chapter explains how to use it and how it works.
   The chapter is contributed by Patrick Loiseleur.