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]
---
 vernac/declareObl.ml | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

(limited to 'vernac')

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