From 2b3bd349914a759b270cea48a7ec32c9320f1792 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 14 Mar 2020 22:41:07 -0400
Subject: [obligations] Deprecated flag cleanup

We deprecate `Hide Obligations` and remove `Shrink Obligations`
[deprecated since 8.7]
---
 .../11828-obligations+depr_hide_obligation.rst               |  9 +++++++++
 doc/sphinx/addendum/program.rst                              | 12 +++---------
 test-suite/success/shrink_obligations.v                      |  2 --
 vernac/declareObl.ml                                         |  9 ++-------
 4 files changed, 14 insertions(+), 18 deletions(-)
 create mode 100644 doc/changelog/07-commands-and-options/11828-obligations+depr_hide_obligation.rst

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 5cffe9e435..d09f23edb6 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 bba3687256..e9fc70cd97 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
-- 
cgit v1.2.3