From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 21 Nov 2006 21:38:49 +0000
Subject: Imported Upstream version 8.1~gamma

---
 doc/refman/Program.tex | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

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

diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index 48ce6bd9..4f8f1281 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}
@@ -507,7 +519,7 @@ generates obligations though it can be useful to insert automatic coercions.
 %  After compilation those two examples run nonetheless,
 %  thanks to the correction of the extraction~\cite{Let02}. 
 
-% $Id: Program.tex 8890 2006-06-01 21:33:26Z msozeau $ 
+% $Id: Program.tex 9332 2006-11-02 12:23:24Z msozeau $ 
 
 %%% Local Variables: 
 %%% mode: latex
-- 
cgit v1.2.3