From fe56933b466a3d833d161828a34aab7a6b621b00 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 11 Jul 2017 17:52:22 +0200
Subject: Sync the manual with the deprecation warnings.

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

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

diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index 2fc1c8764a..f60908da6c 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -278,7 +278,8 @@ 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 should have their
+\emph{Deprecated since 8.7}
+  This option (on by default) controls 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