From 5e93f1e95853c3614df813845b94051a45f1a749 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 22 Nov 2016 17:51:32 +0100 Subject: Deprecate options that were introduced for compatibility with 8.2. --- plugins/ltac/tauto.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins') diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index c6cc955b0f..2a8ed72387 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -79,7 +79,7 @@ let _ = let _ = declare_bool_option - { optdepr = false; + { optdepr = true; (* remove in 8.8 *) optname = "unfolding of iff in intuition"; optkey = ["Intuition";"Iff";"Unfolding"]; optread = (fun () -> !iff_unfolding); -- cgit v1.2.3