Documenting the Set Refine Instance Mode.

2 files changed, 13 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index bf322f6895..b1946188b4 100644
--- a/CHANGES
+++ b/CHANGES
@@ -63,6 +63,8 @@ Vernacular commands
   retrieved using the "Locate Term" command.
 - New "Derive" command to help writing program by derivation.
 - "Undo" undoes any command, not just tactics.
+- New "Refine Instance Mode" option that allows to deactivate the generation of
+  obligations in incomplete typeclass instances, raising an error instead.
 
 Specification Language
 
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 869ba971cc..1d134269f5 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -413,6 +413,17 @@ based on a variant of eauto. The flags semantics are:
 \item {\emph{depth}} This sets the depth of the search (the default is 100).
 \end{itemize}
 
+\subsection{\tt Set Refine Instance Mode}
+\comindex{Set Refine Instance Mode}\comindex{Unset Refine Instance Mode}
+
+The option {\tt Refine Instance Mode} allows to switch the behaviour of instance
+declarations made through the {\tt Instance} command.
+\begin{itemize}
+\item When it is on (the default), instances that have unsolved holes in their
+proof-term silently open the proof mode with the remaining obligations to prove.
+\item When it is off, they fail with an error instead.
+\end{itemize}
+
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"