diff options
Diffstat (limited to 'doc/refman/Program.tex')
| -rw-r--r-- | doc/refman/Program.tex | 16 |
1 files changed, 14 insertions, 2 deletions
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 |