3 files changed, 14 insertions, 8 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.
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index c564346a4e..7d70a7205f 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -211,9 +211,9 @@ tactic is replaced by the default one if not specified.
   obligations (does not work with structurally recursive programs).
 \end{itemize}
 
-The module {\tt Coq.subtac.Utils} defines the default tactic for solving
-obligations called {\tt subtac\_simpl}. Importing it also adds some
-useful notations, as documented in the file itself.
+The module {\tt Coq.Program.Tactics} defines the default tactic for solving
+obligations called {\tt program\_simpl}. Importing 
+{\tt Coq.Program.Program} also adds some useful notations, as documented in the file itself.
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/RefMan-add.tex b/doc/refman/RefMan-add.tex
index e21070d14e..52746fad6e 100644
--- a/doc/refman/RefMan-add.tex
+++ b/doc/refman/RefMan-add.tex
@@ -21,6 +21,12 @@ extract ML program files. It is described in the separate document
 {\tt Extraction.dvi}
 \index{Extraction of programs}
 
+\section[{\tt Program}]{A tool for {\tt Program}-ing\label{Addoc-program}}
+{\tt Program} is a package offering some special facilities to
+extract ML program files. It is described in the separate document
+{\tt Program.dvi}
+\index{Program-ing}
+
 \section[Proof printing in {\tt Natural} language]{Proof printing in {\tt Natural} language\label{Addoc-natural}}
 {\tt Natural} is a tool to print proofs in natural language.
 It is described in the separate document {\tt Natural.dvi}.