From 5e93f1e95853c3614df813845b94051a45f1a749 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Tue, 22 Nov 2016 17:51:32 +0100
Subject: Deprecate options that were introduced for compatibility with 8.2.

---
 vernac/vernacentries.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/vernacentries.ml')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 9978848ff..ba1da655a 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1298,7 +1298,7 @@ let _ =
 
 let _ =
   declare_bool_option
-    { optdepr  = false;
+    { optdepr  = true; (* remove in 8.8 *)
       optname  = "automatic introduction of variables";
       optkey   = ["Automatic";"Introduction"];
       optread  = Flags.is_auto_intros;
-- 
cgit v1.2.3