documentation of commit 10188

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

1 files changed, 9 insertions, 1 deletions

diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index a68969c38..c8daea1dc 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -231,7 +231,7 @@ variables has to be given. The syntax is then:
 \item{\tt Extract Constant \qualid\ \str$_1$ \ldots \str$_n$ => \str.} ~\par
 \end{description}
 
-The number of type variable given is checked by the system. 
+The number of type variables is checked by the system. 
 
 \Example
 \begin{coq_example}
@@ -274,6 +274,14 @@ Extract Inductive bool => "bool" [ "true" "false" ].
 Extract Inductive sumbool => "bool" [ "true" "false" ].
 \end{coq_example}
 
+If an inductive constructor or type has arity 2 and the corresponding 
+string is enclosed by parenthesis, then the rest of the string is used
+as infix constructor or type. 
+\begin{coq_example}
+Extract Inductive list => "list" [ "[]" "(::)" ].
+Extract Inductive prod => "(*)"  [ "(,)" ].
+\end{coq_example}
+
 
 \asection{Differences between \Coq\ and ML type systems}