Minor fixes:

- Document and fix [autounfold]
- Fix warning about default Firstorder tactic object not being defined
- Fix treatment of implicits in Program Lemma.


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

1 files changed, 18 insertions, 0 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 07921978d5..5a1014dae5 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3207,6 +3207,24 @@ hint.
 
 \SeeAlso Section~\ref{Hints-databases}
 
+\subsection{\tt autounfold with  \ident$_1$ \dots\ \ident$_n$
+\tacindex{autounfold}
+\label{autounfold}}
+
+This tactic unfolds constants that were declared through a {\tt Hint
+  Unfold} in the given databases.
+
+\begin{Variants}
+\item {\tt autounfold with \ident$_1$ \dots\ \ident$_n$ in \textit{clause}}
+  
+  Perform the unfolding in the given clause.
+
+\item {\tt autounfold with *}
+  
+  Uses the unfold hints declared in all the hint databases.
+\end{Variants}
+
+
 % EXISTE ENCORE ?
 % 
 % \subsection{\tt Prolog [ \term$_1$ \dots\ \term$_n$ ] \num}