From df6c304249d89525dd79f2dc14df60c44225bac6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 15 Apr 2004 16:13:14 +0000
Subject: In�l�gance de notation du match

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8547 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/RefMan-ext.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/RefMan-ext.tex b/doc/RefMan-ext.tex
index c9bcd3b38f..192e1f2dc9 100644
--- a/doc/RefMan-ext.tex
+++ b/doc/RefMan-ext.tex
@@ -327,8 +327,8 @@ The general equivalence for an inductive type with one constructors {\tt C} is
 
 \smallskip
 {\tt let ({\ident}$_1$,\ldots,{\ident}$_n$) \zeroone{\ifitem} := {\term} in {\term}'} \\
-$\equiv\;$
-{\tt match {\term} \zeroone{\ifitem} with \verb!|! C {\ident}$_1$ {\ldots} {\ident}$_n$ \verb!=>! {\term}' end}
+$\equiv$~
+{\tt match {\term} \zeroone{\ifitem} with C {\ident}$_1$ {\ldots} {\ident}$_n$ \verb!=>! {\term}' end}
 
 \subsection{Options for pretty-printing of {\tt match}
 \label{printing-options}}
-- 
cgit v1.2.3