Merge PR #13188: Default disable automatic generalization of Instance type

Ack-by: Blaisorblade
Reviewed-by: JasonGross
Reviewed-by: Zimmi48
Ack-by: jfehrle
Reviewed-by: ppedrot

2 files changed, 16 insertions, 0 deletions

diff --git a/doc/changelog/02-specification-language/13188-instance-gen.rst b/doc/changelog/02-specification-language/13188-instance-gen.rst
new file mode 100644
index 0000000000..6a431f85ed
--- /dev/null
+++ b/doc/changelog/02-specification-language/13188-instance-gen.rst
@@ -0,0 +1,6 @@
+- **Removed:** The type given to :cmd:`Instance` is no longer automatically
+  generalized over unbound and :ref:`generalizable <implicit-generalization>` variables.
+  Use :n:`Instance : \`{@type}` instead of :n:`Instance : @type` to get the old behaviour, or
+  enable the compatibility flag :flag:`Instance Generalized Output`.
+  (`#13188 <https://github.com/coq/coq/pull/13188>`_, fixes `#6042
+  <https://github.com/coq/coq/issues/6042>`_, by Gaëtan Gilbert).
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 56d90b33d8..2474c784b8 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -391,6 +391,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`.