Merge PR #6903: [compat] Remove "Shrink Abstract"

3 files changed, 1 insertions, 28 deletions

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index c4c0435c5f..0a4d0ef9aa 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.
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b99a451030..b41df7f757 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -89,18 +89,6 @@ let _ =
       optread  = (fun () -> !universal_lemma_under_conjunctions) ;
       optwrite = (fun b -> universal_lemma_under_conjunctions := b) }
 
-(* Shrinking of abstract proofs. *)
-
-let shrink_abstract = ref true
-
-let _ =
-  declare_bool_option
-    { optdepr  = true; (* remove in 8.8 *)
-      optname  = "shrinking of abstracted proofs";
-      optkey   = ["Shrink"; "Abstract"];
-      optread  = (fun () -> !shrink_abstract) ;
-      optwrite = (fun b -> shrink_abstract := b) }
-
 (* The following boolean governs what "intros []" do on examples such
    as "forall x:nat*nat, x=x"; if true, it behaves as "intros [? ?]";
    if false, it behaves as "intro H; case H; clear H" for fresh H.
@@ -4986,10 +4974,7 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
     let (_, info) = CErrors.push src in
     iraise (e, info)
   in
-  let const, args =
-    if !shrink_abstract then shrink_entry sign const
-    else (const, List.rev (Context.Named.to_instance Constr.mkVar sign))
-  in
+  let const, args = shrink_entry sign const in
   let args = List.map EConstr.of_constr args in
   let cd = Entries.DefinitionEntry { const with Entries.const_entry_opaque = opaque } in
   let decl = (cd, if opaque then IsProof Lemma else IsDefinition Definition) in
diff --git a/test-suite/success/shrink_abstract.v b/test-suite/success/shrink_abstract.v
index 3f6b9cb39f..916bb846a9 100644
--- a/test-suite/success/shrink_abstract.v
+++ b/test-suite/success/shrink_abstract.v
@@ -1,5 +1,3 @@
-Set Shrink Abstract.
-
 Definition foo : forall (n m : nat), bool.
 Proof.
 pose (p := 0).