diff options
| author | Théo Zimmermann | 2017-07-04 17:11:45 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2017-07-11 16:27:56 +0200 |
| commit | fbbcea2eda411fbacfafdeec3266a19af17935f3 (patch) | |
| tree | 24c4d298f6a0a5f294518c450d0dc98f59417bd3 /vernac | |
| parent | ba7129f547d1f06c7eb67412404445681d22b920 (diff) | |
Deprecate options that were introduced for compatibility with 8.5.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/obligations.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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; |