Documenting the previous commit: Existing Instance with priority.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16646 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 6 deletions

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index f7c4bd5caf..ea1ae02bcb 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -357,18 +357,19 @@ priority as for auto hints.
 Besides the {\tt Class} and {\tt Instance} vernacular commands, there
 are a few other commands related to type classes.
 
-\subsection{\tt Existing Instance {\ident}}
+\subsection{\tt Existing Instance {\ident} [| \textit{priority}]}
 \comindex{Existing Instance}
 \label{ExistingInstance}
 
 This commands adds an arbitrary constant whose type ends with an applied
-type class to the instance database. It can be used for redeclaring
-instances at the end of sections, or declaring structure projections as
-instances. This is almost equivalent to {\tt Hint Resolve {\ident} :
-  typeclass\_instances}.
+type class to the instance database with an optional priority. It can be used
+for redeclaring instances at the end of sections, or declaring structure
+projections as instances. This is almost equivalent to {\tt Hint Resolve
+{\ident} : typeclass\_instances}.
 
 \begin{Variants}
-\item {\tt Existing Instances {\ident}$_1$ \ldots {\ident}$_n$}
+\item {\tt Existing Instances {\ident}$_1$ \ldots {\ident}$_n$
+  [| \textit{priority}]}
   \comindex{Existing Instances}
   With this command, several existing instances can be declared at once.
 \end{Variants}