diff options
Diffstat (limited to 'doc/refman/Program.tex')
| -rw-r--r-- | doc/refman/Program.tex | 14 |
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} |