From e0d870a48a319a49d6061164733016fde65ab8f6 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 1 Nov 2019 13:04:59 -0400
Subject: Update the deprecation doc of `Shrink Obligations`

Now it uses `.. deprecated` like all the other deprecation notices in
the manual.
---
 doc/sphinx/addendum/program.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/sphinx')

diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index 45c74ab02a..69e442f399 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -341,7 +341,7 @@ optional tactic is replaced by the default one if not specified.
 
 .. flag:: Shrink Obligations
 
-   *Deprecated since 8.7*
+   .. deprecated:: 8.7
 
    This option (on by default) controls whether obligations should have
    their context minimized to the set of variables used in the proof of
-- 
cgit v1.2.3