aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/ltac/tauto.ml2
1 files changed, 1 insertions, 1 deletions
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);