diff options
| author | Jason Gross | 2019-11-01 13:04:59 -0400 |
|---|---|---|
| committer | Jason Gross | 2019-11-01 13:04:59 -0400 |
| commit | e0d870a48a319a49d6061164733016fde65ab8f6 (patch) | |
| tree | d56626513d35f7eec4825b09a4f54cc651bb283e | |
| parent | fdabd4dbd6bfd60ad46fc8c945ed063860498e53 (diff) | |
Update the deprecation doc of `Shrink Obligations`
Now it uses `.. deprecated` like all the other deprecation notices in
the manual.
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 2 |
1 files changed, 1 insertions, 1 deletions
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 |