From 7a7a09378e492b5b2dc87e3a8e502e842ca1faf5 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 6 Apr 2011 11:38:31 +0000
Subject: 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
---
 doc/refman/Classes.tex | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'doc')

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