From 59ea396dc5fd01afd8f8dfd8ec18f84d787244c0 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 2 Nov 2020 14:36:07 +0100
Subject: Doc and changelog for Instance Generalized Output

---
 doc/sphinx/addendum/type-classes.rst | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'doc/sphinx/addendum')

diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index cdd31fcb86..e311544c86 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -388,6 +388,16 @@ Summary of the commands
       equivalent to ``Hint Resolve ident : typeclass_instances``, except it
       registers instances for :cmd:`Print Instances`.
 
+   .. flag:: Instance Generalized Output
+
+      .. deprecated:: 8.13
+
+      Disabled by default, this provides compatibility with Coq
+      version 8.12 and earlier.
+
+      When enabled, the type of the instance is implicitly generalized
+      over unbound and :ref:`generalizable <implicit-generalization>` variables as though surrounded by ``\`{}``.
+
 .. cmd:: Print Instances @reference
 
    Shows the list of instances associated with the typeclass :token:`reference`.
-- 
cgit v1.2.3