From ea3763f3bc406dd3257e1d8ec4d489a0790ae713 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 8 Aug 2007 13:14:05 +0000
Subject: 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
---
 doc/refman/Program.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc/refman/Program.tex')

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
-- 
cgit v1.2.3