12 files changed, 35 insertions, 15 deletions
diff --git a/doc/Makefile b/doc/Makefile
index 143fc2e29..99e075f0a 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -214,7 +214,7 @@ faq/html/index.html: faq/FAQ.v.html
 
 GLOBDUMP=$(COQTOP)/glob.dump
 
-LIBDIRS= Init Logic Bool Arith NArith ZArith QArith Relations Sets Setoids Lists Sorting Wellfounded IntMap FSets Reals 
+LIBDIRS= Init Logic Bool Arith NArith ZArith QArith Relations Sets Setoids Lists Sorting Wellfounded IntMap FSets Reals Program
 # We avoid Strings as String.v contains unicode caracters that make latex fail
 
 LIBDIRS+= Ints Ints/num
diff --git a/doc/refman/AddRefMan-pre.tex b/doc/refman/AddRefMan-pre.tex
index 15776690c..85811c145 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 c564346a4..7d70a7205 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 e21070d14..52746fad6 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}.
diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex
index fffcddc85..81fdd2a6e 100755
--- a/doc/stdlib/Library.tex
+++ b/doc/stdlib/Library.tex
@@ -45,6 +45,8 @@ The standard library is composed of the following subdirectories:
   \item[Wellfounded] Well-founded relations (basic results).
   \item[IntMap]       Representation of finite sets by an efficient
                      structure of map (trees indexed by binary integers).
+  \item[Program] Tactcis to deal with dependently-typed programs and
+    their proofs.
 \end{description}
 
 
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 2a8693438..65d69a1d8 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -402,5 +402,17 @@ through the <tt>Require Import</tt> command.</p>
     theories/Ints/num/ZnZ.v
   </dd>
 
+    
+  <dt> <b>Program</b>:
+    Support for dependently-typed programming.
+  </dt>
+  <dd> 
+    theories/Program/Wf.v
+    theories/Program/Equality.v
+    theories/Program/Tactics.v
+    theories/Program/Utils.v
+    theories/Program/Program.v
+    theories/Program/FunctionalExtensionality.v
+  </dd>
 
 </dl>
diff --git a/doc/stdlib/make-library-files b/doc/stdlib/make-library-files
index 91e3cc3f4..6eb1333a5 100755
--- a/doc/stdlib/make-library-files
+++ b/doc/stdlib/make-library-files
@@ -10,7 +10,7 @@
 # En supposant que make fait son boulot, ca fait un tri topologique du
 # graphe des dépendances
 
-LIBDIRS="Arith NArith ZArith Reals Logic Bool Lists IntMap Relations Sets Sorting Wellfounded Setoids"
+LIBDIRS="Arith NArith ZArith Reals Logic Bool Lists IntMap Relations Sets Sorting Wellfounded Setoids Program"
 
 rm -f library.files.ls.tmp
 (cd $COQTOP/theories; find $LIBDIR -name "*.v" -ls) > library.files.ls.tmp
diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index
index cbcd15ef3..27dfc434f 100755
--- a/doc/stdlib/make-library-index
+++ b/doc/stdlib/make-library-index
@@ -7,7 +7,7 @@ FILE=$1
 cp -f $FILE.template tmp
 echo -n Building file index-list.prehtml ...
 
-LIBDIRS="Init Logic Bool Arith NArith ZArith QArith Relations Sets Setoids Lists Sorting Wellfounded IntMap FSets Reals Ints Ints/num"
+LIBDIRS="Init Logic Bool Arith NArith ZArith QArith Relations Sets Setoids Lists Sorting Wellfounded IntMap FSets Reals Ints Ints/num Program"
 
 for k in $LIBDIRS; do
     i=../theories/$k
diff --git a/theories/Program/Heq.v b/theories/Program/Equality.v
index cd405219f..cd405219f 100644
--- a/theories/Program/Heq.v
+++ b/theories/Program/Equality.v
diff --git a/theories/Program/FunctionalExtensionality.v b/theories/Program/FunctionalExtensionality.v
index c6e5a64fb..40356a9c4 100644
--- a/theories/Program/FunctionalExtensionality.v
+++ b/theories/Program/FunctionalExtensionality.v
@@ -1,5 +1,5 @@
 Require Import Coq.Program.Utils.
-Require Import Coq.Program.FixSub.
+Require Import Coq.Program.Wf.
 
 (** The converse of functional equality. *)
 
diff --git a/theories/Program/Program.v b/theories/Program/Program.v
index 4dc50694f..39c5b7734 100644
--- a/theories/Program/Program.v
+++ b/theories/Program/Program.v
@@ -1,3 +1,3 @@
 Require Export Coq.Program.Utils.
-Require Export Coq.Program.FixSub.
-Require Export Coq.Program.Heq.
-\ No newline at end of file
+Require Export Coq.Program.Wf.
+Require Export Coq.Program.Equality.
diff --git a/theories/Program/FixSub.v b/theories/Program/Wf.v
index 58ac9d90e..55784671f 100644
--- a/theories/Program/FixSub.v
+++ b/theories/Program/Wf.v
@@ -1,4 +1,4 @@
-Require Import Wf.
+Require Import Coq.Init.Wf.
 Require Import Coq.Program.Utils.
 Require Import ProofIrrelevance.