Add 'Existing Instances' declaration to declare multiple instances at once.

This is useful, for example, in declaring the projection of the dependent
record bundled form of an unbundled typeclass.

Patch submitted by Tom Prince

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

1 files changed, 6 insertions, 0 deletions

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 7bd4f3522d..20ff649aac 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -367,6 +367,12 @@ 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$}
+  \comindex{Existing Instances}
+  With this command, several existing instances can be declared at once.
+\end{Variants}
+
 \subsection{\tt Context {\binder$_1$ \ldots \binder$_n$}}
 \comindex{Context}
 \label{Context}