From 9510a3994210f545119ea35cdad43facededb6a2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 8 Sep 2015 11:27:17 +0200
Subject: Documenting the new behaviour of the Shrink Obligations flag.

---
 doc/refman/Program.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/refman/Program.tex')

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}
-- 
cgit v1.2.3