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 0f6a5cbf6c..3580684a73 100644 --- a/doc/refman/Program.tex +++ b/doc/refman/Program.tex @@ -207,7 +207,7 @@ obligations (e.g. when defining mutually recursive blocks). The optional tactic is replaced by the default one if not specified. \begin{itemize} -\item {\tt Obligations Tactic := \tacexpr}\comindex{Obligations Tactic} +\item {\tt Obligation Tactic := \tacexpr}\comindex{Obligation Tactic} Sets the default obligation solving tactic applied to all obligations automatically, whether to solve them or when starting to prove one, e.g. using {\tt Next}. |