diff options
Diffstat (limited to 'doc/refman/Program.tex')
| -rw-r--r-- | doc/refman/Program.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex index ea694f61d2..2025164f2e 100644 --- a/doc/refman/Program.tex +++ b/doc/refman/Program.tex @@ -174,7 +174,7 @@ The following commands are available to manipulate obligations: each obligation using the given tactic. \item {\tt Admit Obligations [of \ident]} Admits all obligations (does not work with structurally recursive programs). -\item {\tt Obligations Tactic := \expr} Sets the default obligation +\item {\tt Obligations Tactic := \tacexpr} Sets the default obligation solving tactic applied to all obligations. \end{itemize} |