Add doc on obligation solving commands.

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

1 files changed, 13 insertions, 1 deletions

diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index e9343489b4..723936f5b9 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -134,7 +134,7 @@ Program Fixpoint div2 (n : nat) : { x : nat | n = 2 * x \/ n = 2 * x + 1 } :=
 Here we have one obligation for each branch (branches for \verb:0: and \verb:(S 0): are
 automatically generated by the pattern-matching compilation algorithm):
 \begin{coq_example}
-  Show.
+  Obligations.
 \end{coq_example}
 
 \subsection{\tt Program Lemma {\ident} : type.
@@ -145,6 +145,18 @@ The \Russell\ language can also be used to type statements of logical
 properties. It will currently fail if the traduction to \Coq\
 generates obligations though it can be useful to insert automatic coercions.
 
+\subsection{Solving obligations}
+The following commands are available to manipulate obligations:
+
+\begin{itemize}
+\item {\tt Obligations [of \ident]} Displays all remaining
+  obligations.
+\item {\tt Solve Obligation num [of \ident]} Start the proof of
+  obligation {\tt num}.
+\item {\tt Solve Obligations [of \ident] using} {\tacexpr} Tries to solve
+  each obligation using the given tactic.
+\end{itemize}
+  
 
 % \subsection{\tt Program Fixpoint {\ident} {(\ident_$_0$ : \type_$_0$)
 %     \cdots (\ident_$_n$ : \type_$_n$)} {\tt \{wf}