From 676348579e907c09f575863b5afba42f5478041a Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 22 Mar 2019 20:54:51 +0100
Subject: Deprecate `Refine Instance Mode` option

This is in view of the 8.10 release, after which we will remove the
option and the `VtUnknown` classification.
---
 CHANGES.md                           | 3 +++
 doc/sphinx/addendum/type-classes.rst | 2 ++
 vernac/classes.ml                    | 2 +-
 3 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/CHANGES.md b/CHANGES.md
index dcf321c7ff..d43dc668e8 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -153,6 +153,9 @@ Vernacular commands
 
 - The `Show Script` command has been deprecated.
 
+- Option `Refine Instance Mode` has been deprecated and will be removed in
+  the next version.
+
 Tools
 
 - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values:
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index e6a5b3972c..0a480bdbe7 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -561,6 +561,8 @@ Settings
 
 .. flag:: Refine Instance Mode
 
+   .. deprecated:: 8.10
+
    This flag allows to switch the behavior of instance declarations made through
    the Instance command.
 
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 1981e24ae4..61b8cc3dcb 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -31,7 +31,7 @@ open Entries
 let refine_instance = ref false
 
 let () = Goptions.(declare_bool_option {
-  optdepr  = false;
+  optdepr  = true;
   optname  = "definition of instances by refining";
   optkey   = ["Refine";"Instance";"Mode"];
   optread  = (fun () -> !refine_instance);
-- 
cgit v1.2.3