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

4 files changed, 9 insertions, 4 deletions

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 5966ac468c..7e07868a38 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -486,15 +486,17 @@ where there is a hole in that place.
 
 \subsection{\tt Set Typeclasses Legacy Resolution}
 \optindex{Typeclasses Legacy Resolution}
+\emph{Deprecated since 8.7}
 
 This option (off by default) uses the 8.5 implementation of resolution.
 Use for compatibility purposes only (porting and debugging).
 
 \subsection{\tt Set Typeclasses Module Eta}
 \optindex{Typeclasses Modulo Eta}
+\emph{Deprecated since 8.7}
 
 This option allows eta-conversion for functions and records during
-unification of type-classes. This option is now unsupported in 8.6 with
+unification of type-classes. This option is unsupported since 8.6 with
 {\tt Typeclasses Filtered Unification} set, but still affects the
 default unification strategy, and the one used in {\tt Legacy
   Resolution} mode. It is \emph{unset} by default. If {\tt Typeclasses
@@ -505,7 +507,7 @@ pattern-matching is not up-to eta.
 \subsection{\tt Set Typeclasses Limit Intros}
 \optindex{Typeclasses Limit Intros}
 
-This option (on by default in Coq 8.6 and below) controls the ability to
+This option (on by default) controls the ability to
 apply hints while avoiding (functional) eta-expansions in the generated
 proof term. It does so by allowing hints that conclude in a product to
 apply to a goal with a matching product directly, avoiding an
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}
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index f3bc2dd05e..3ce1d4ecd8 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1131,8 +1131,9 @@ on. This can be obtained thanks to the option below.
 \optindex{Shrink Abstract}
 {\tt Set Shrink Abstract}
 \end{quote}
+\emph{Deprecated since 8.7}
 
-When set, all lemmas generated through \texttt{abstract {\tacexpr}}
+When set (default), all lemmas generated through \texttt{abstract {\tacexpr}}
 and \texttt{transparent\_abstract {\tacexpr}} are quantified only over the
 variables that appear in the term constructed by \texttt{\tacexpr}.
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index ecb89b5fb8..a23c432322 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3485,6 +3485,7 @@ reduced to \texttt{S t}.
 \optindex{Refolding Reduction}
 {\tt Refolding Reduction}
 \end{quote}
+\emph{Deprecated since 8.7}
 
 This option (off by default) controls the use of the refolding strategy
 of {\tt cbn} while doing reductions in unification, type inference and