diff options
Diffstat (limited to 'doc')
| -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 |