diff options
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 4b1565d3ce..10d3317f8d 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; |