From 180b3739bb6601ff9aaf951e4b87e0bb45341b77 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Tue, 22 Nov 2016 17:54:14 +0100
Subject: Deprecate options that were introduced for compatibility with 8.4.

---
 engine/namegen.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine/namegen.ml')

diff --git a/engine/namegen.ml b/engine/namegen.ml
index e635dc163..783085654 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -417,7 +417,7 @@ let use_h_based_elimination_names () = !h_based_elimination_names
 open Goptions
 
 let _ = declare_bool_option
-	  { optdepr  = false;
+	  { optdepr  = true; (* remove in 8.8 *)
 	    optname  = "use of \"H\"-based proposition names in elimination tactics";
 	    optkey   = ["Standard";"Proposition";"Elimination";"Names"];
 	    optread  = (fun () -> !h_based_elimination_names);
-- 
cgit v1.2.3