Merge PR #855: Deprecate options that were introduced for compatibility with 8.5.

1 files changed, 2 insertions, 1 deletions

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}