From fbbcea2eda411fbacfafdeec3266a19af17935f3 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 4 Jul 2017 17:11:45 +0200
Subject: Deprecate options that were introduced for compatibility with 8.5.

---
 vernac/obligations.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index c0acdaf57d..5647a9c4f7 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -350,7 +350,7 @@ let get_shrink_obligations () = !shrink_obligations
 
 let _ =
   declare_bool_option
-    { optdepr  = true;
+    { optdepr  = true; (* remove in 8.8 *)
       optname  = "Shrinking of Program obligations";
       optkey   = ["Shrink";"Obligations"];
       optread  = get_shrink_obligations;
-- 
cgit v1.2.3