From 524f38b37fa744b7859d8c97bdec6bcbf27882aa Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 30 Nov 2014 04:25:49 +0100
Subject: Documenting the Set Refine Instance Mode.

---
 doc/refman/Classes.tex | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'doc')

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"
-- 
cgit v1.2.3