From fe902cb9235a29427f18c234ffffc9b9070512a1 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Mon, 5 Mar 2018 13:40:18 +0100
Subject: [compat] Remove "Shrink Abstract"

Following up on #6791, we the option "Shrink Abstract".
---
 doc/refman/RefMan-ltac.tex | 10 ----------
 1 file changed, 10 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index c4c0435c5..0a4d0ef9a 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1156,16 +1156,6 @@ without having to cut manually the proof in smaller lemmas.
 It may be useful to generate lemmas minimal w.r.t. the assumptions they depend
 on. This can be obtained thanks to the option below.
 
-\begin{quote}
-\optindex{Shrink Abstract}
-{\tt Set Shrink Abstract}
-\end{quote}
-\emph{Deprecated since 8.7}
-
-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}.
-
 \begin{Variants}
 \item \texttt{abstract {\tacexpr} using {\ident}}.\\
   Give explicitly the name of the auxiliary lemma.
-- 
cgit v1.2.3