Merge PR #10996: Refine Instance returns

Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: ppedrot

2 files changed, 20 insertions, 3 deletions

diff --git a/doc/changelog/02-specification-language/10996-refine-instance-returns.rst b/doc/changelog/02-specification-language/10996-refine-instance-returns.rst
new file mode 100644
index 0000000000..cd1a692f54
--- /dev/null
+++ b/doc/changelog/02-specification-language/10996-refine-instance-returns.rst
@@ -0,0 +1,4 @@
+- Added ``#[refine]`` attribute for :cmd:`Instance`, a more
+  predictable version of the old ``Refine Instance Mode`` which
+  unconditionally opens a proof (`#10996
+  <https://github.com/coq/coq/pull/10996>`_, by Gaëtan Gilbert).
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 1bbf988505..57a2254100 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -47,9 +47,22 @@ Leibniz equality on some type. An example implementation is:
          | tt, tt => eq_refl tt
          end }.
 
-Using :cmd:`Program Instance`, if one does not give all the members in
-the Instance declaration, Coq generates obligations for the remaining
-fields, e.g.:
+Using the attribute ``refine``, if the term is not sufficient to
+finish the definition (e.g. due to a missing field or non-inferable
+hole) it must be finished in proof mode. If it is sufficient a trivial
+proof mode with no open goals is started.
+
+.. coqtop:: in
+
+   #[refine] Instance unit_EqDec' : EqDec unit := { eqb x y := true }.
+   Proof. intros [] [];reflexivity. Defined.
+
+Note that if you finish the proof with :cmd:`Qed` the entire instance
+will be opaque, including the fields given in the initial term.
+
+Alternatively, in :flag:`Program Mode` if one does not give all the
+members in the Instance declaration, Coq generates obligations for the
+remaining fields, e.g.:
 
 .. coqtop:: in