From 68bdefae23d4175b523f4857faab254d9902083c Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 2 Dec 2019 08:43:38 +0100
Subject: Highlight refine attribute for Instance.

---
 doc/sphinx/changes.rst | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index f221f0ed7d..47899ea1ed 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -32,6 +32,8 @@ The main changes brought by |Coq| version 8.11 are:
   dependencies.
 - New :g:`Arguments` annotation for `bidirectional type inference`__
   configuration for reference (e.g. constants, inductive) applications.
+- New `refine attribute`__ for :cmd:`Instance` can be used instead of
+  the removed ``Refine Instance Mode``.
 - Generalization of the :g:`under` and :g:`over` tactics__ of SSReflect to
   arbitrary relations.
 - `Revision`__ of the :g:`Coq.Reals` library, its axiomatisation and
@@ -44,6 +46,7 @@ __ 811UnsafeFlags_
 __ 811ExportBug_
 __ 811vos_
 __ 811BidirArguments_
+__ 811RefineInstance_
 __ 811SSRUnderOver_
 __ 811Reals_
 
@@ -194,6 +197,9 @@ Changes in 8.11+beta1
   :cmd:`Arguments <Arguments (implicits)>` command instead of the
   human-targeted prose used in previous Coq versions. (`#10985
   <https://github.com/coq/coq/pull/10985>`_, by Gaëtan Gilbert).
+
+  .. _811RefineInstance:
+
 - **Added:** ``#[refine]`` attribute for :cmd:`Instance`, a more
   predictable version of the old ``Refine Instance Mode`` which
   unconditionally opens a proof (`#10996
-- 
cgit v1.2.3