Merge PR #11828: [obligations] Deprecated flag cleanup

Reviewed-by: SkySkimmer
Ack-by: Zimmi48

4 files changed, 14 insertions, 18 deletions

diff --git a/doc/changelog/07-commands-and-options/11828-obligations+depr_hide_obligation.rst b/doc/changelog/07-commands-and-options/11828-obligations+depr_hide_obligation.rst
new file mode 100644
index 0000000000..5ab2941446
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/11828-obligations+depr_hide_obligation.rst
@@ -0,0 +1,9 @@
+- **Deprecated:**
+  Option :flag:`Hide Obligations` has been deprecated
+  (`#11828 <https://github.com/coq/coq/pull/11828>`_,
+  by Emilio Jesus Gallego Arias).
+
+- **Removed:**
+  Deprecated option ``Shrink Obligations`` has been removed
+  (`#11828 <https://github.com/coq/coq/pull/11828>`_,
+  by Emilio Jesus Gallego Arias).
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index 52862dea47..b5618c5721 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -342,17 +342,11 @@ optional tactic is replaced by the default one if not specified.
 
 .. flag:: Hide Obligations
 
+   .. deprecated:: 8.12
+
    Controls whether obligations appearing in the
    term should be hidden as implicit arguments of the special
-   constantProgram.Tactics.obligation.
-
-.. flag:: Shrink Obligations
-
-   .. deprecated:: 8.7
-
-   This flag (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.
+   constant ``Program.Tactics.obligation``.
 
 The module :g:`Coq.Program.Tactics` defines the default tactic for solving
 obligations called :g:`program_simpl`. Importing :g:`Coq.Program.Program` also
diff --git a/test-suite/success/shrink_obligations.v b/test-suite/success/shrink_obligations.v
index 676b97878f..032fcaac6d 100644
--- a/test-suite/success/shrink_obligations.v
+++ b/test-suite/success/shrink_obligations.v
@@ -2,8 +2,6 @@ Require Program.
 
 Obligation Tactic := idtac.
 
-Set Shrink Obligations.
-
 Program Definition foo (m : nat) (p := S m) (n : nat) (q := S n) : unit :=
 let bar : {r | n < r} := _ in
 let qux : {r | p < r} := _ in
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index ab11472dec..9ea54f5d8f 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -111,11 +111,6 @@ open ProgramDecl
 
 (* Saving an obligation *)
 
-let get_shrink_obligations =
-  Goptions.declare_bool_option_and_ref ~depr:true (* remove in 8.8 *)
-    ~key:["Shrink"; "Obligations"]
-    ~value:true
-
 (* XXX: Is this the right place for this? *)
 let it_mkLambda_or_LetIn_or_clean t ctx =
   let open Context.Rel.Declaration in
@@ -190,7 +185,7 @@ let add_hint local prg cst =
 (* true = hide obligations *)
 let get_hide_obligations =
   Goptions.declare_bool_option_and_ref
-    ~depr:false
+    ~depr:true
     ~key:["Hide"; "Obligations"]
     ~value:false
 
@@ -203,7 +198,7 @@ let declare_obligation prg obl body ty uctx =
     let opaque = (not force) && opaque in
     let poly = prg.prg_poly in
     let ctx, body, ty, args =
-      if get_shrink_obligations () && not poly then shrink_body body ty
+      if not poly then shrink_body body ty
       else ([], body, ty, [||])
     in
     let ce = Declare.definition_entry ?types:ty ~opaque ~univs:uctx body in