Applying François Garillot's patch (#2261 in bug tracker) for extended

syntax of "Implicit Type" (that can now be "Implicit Types" and can
now accept several blocks of variables of a given type).

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

1 files changed, 6 insertions, 0 deletions

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 42374e368..01df199ab 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1585,6 +1585,12 @@ Lemma cons_inj_bool : forall (m n:bool) l, n :: l = m :: l -> n = m.
 \begin{Variants}
 \item {\tt Implicit Type {\ident} : {\type}}\\
 This is useful for declaring the implicit type of a single variable.
+\item
+ {\tt Implicit Types\,%
+(\,{\ident$_{1,1}$}\ldots{\ident$_{1,k_1}$}\,{\tt :}\,{\term$_1$} {\tt )}\,%
+\ldots\,{\tt (}\,{\ident$_{n,1}$}\ldots{\ident$_{n,k_n}$}\,{\tt :}\,%
+{\term$_n$} {\tt )}.}\\ 
+  Adds $n$ blocks of implicit types with different specifications.
 \end{Variants}