From c4b2e6587c536b00d76ab98df80c1c8a18d0bd0b Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 2 Nov 2006 12:23:24 +0000
Subject: Add doc on obligation solving commands.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9332 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/Program.tex | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

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

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