From f77d428c11bf47c20b8ea67d8ed7dce6af106bcd Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 22 Apr 2010 13:51:03 +0000
Subject: 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
---
 doc/refman/RefMan-ext.tex | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'doc')

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 42374e368f..01df199ab9 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}
 
 
-- 
cgit v1.2.3