Suppression des references a Match/Case

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

1 files changed, 20 insertions, 20 deletions

diff --git a/doc/RefMan-ext.tex b/doc/RefMan-ext.tex
index 24aaa08667..0ed20012e8 100644
--- a/doc/RefMan-ext.tex
+++ b/doc/RefMan-ext.tex
@@ -409,26 +409,26 @@ Unset Printing Wildcard.
 Print snd.
 \end{coq_example}
 
-\subsection{Still not dead old notations}
-
-The following variant of {\tt Cases} is inherited from older version
-of {\Coq}. 
-
-\medskip
-\begin{tabular}{lcl}
-{\term} & ::= & {\annotation} {\tt Match} {\term} {\tt with} {\terms} {\tt end}\\
-\end{tabular}
-\medskip
-
-This syntax is a macro generating a combination of {\tt Cases} with {\tt
-Fix} implementing a combinator for primitive recursion equivalent to
-the {\tt Match} construction of \Coq\ V5.8. It is provided only for
-sake of compatibility with \Coq\ V5.8. It is recommended to avoid it.
-(see section~\ref{Matchexpr}).
-
-There is also a notation \texttt{Case} that is the
-ancestor of \texttt{Cases}. Again, it is still in the code for
-compatibility with old versions but the user should not use it.
+% \subsection{Still not dead old notations}
+
+% The following variant of {\tt Cases} is inherited from older version
+% of {\Coq}. 
+
+% \medskip
+% \begin{tabular}{lcl}
+% {\term} & ::= & {\annotation} {\tt Match} {\term} {\tt with} {\terms} {\tt end}\\
+% \end{tabular}
+% \medskip
+
+% This syntax is a macro generating a combination of {\tt Cases} with {\tt
+% Fix} implementing a combinator for primitive recursion equivalent to
+% the {\tt Match} construction of \Coq\ V5.8. It is provided only for
+% sake of compatibility with \Coq\ V5.8. It is recommended to avoid it.
+% (see section~\ref{Matchexpr}).
+
+% There is also a notation \texttt{Case} that is the
+% ancestor of \texttt{Cases}. Again, it is still in the code for
+% compatibility with old versions but the user should not use it.
 
 \section{Forced type}