diff options
| author | Clément Pit-Claudel | 2019-11-01 16:57:57 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2019-11-01 16:57:57 -0400 |
| commit | b0fe318ea3b54f6f5f4c911bfb0e8523405e8c5c (patch) | |
| tree | 5039c1476a88c50bb62c0c98748abc8e1920332c | |
| parent | 66c7622ba84284135dc821ab5eee7f79102e0c59 (diff) | |
| parent | e0d870a48a319a49d6061164733016fde65ab8f6 (diff) | |
Merge PR #11028: Update the deprecation doc of `Shrink Obligations`
| -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 |