Documenting the new behaviour of the Shrink Obligations flag.

1 files changed, 1 insertions, 1 deletions

diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index 8e078e9814..efcc84ee98 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -261,7 +261,7 @@ tactic is replaced by the default one if not specified.
   as implicit arguments of the special constant
   \texttt{Program.Tactics.obligation}.
 \item {\tt Set Shrink Obligations}\optindex{Shrink Obligations}
-  Control whether obligations defined by tactics should have their
+  Control whether obligations should have their
   context minimized to the set of variables used in the proof of the
   obligation, to avoid unnecessary dependencies.
 \end{itemize}