From 0ebf78fb3bf0300312c22ee708e111c0a2f4be30 Mon Sep 17 00:00:00 2001
From: mohring
Date: Thu, 27 Nov 2003 12:42:06 +0000
Subject: Reparation bug compil

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

diff --git a/doc/syntax-v8.tex b/doc/syntax-v8.tex
index 76fe0e5064..031f59885a 100644
--- a/doc/syntax-v8.tex
+++ b/doc/syntax-v8.tex
@@ -541,8 +541,8 @@ Conflicts exists between integers and constrs.
 \SEPDEF
 \DEFNT{clause}
        \KWD{in}~\TERM{*}
-\nlsep \KWD{in}~\TERM{*}~\KWD{\vdash}~\OPT{\NT{concl-occ}}
-\nlsep \KWD{in}~\OPT{\TERM{hyp-ident-list}} ~\KWD{\vdash} ~\OPT{\NT{concl-occ}}
+\nlsep \KWD{in}~\TERM{*}~\KWD{$\vdash$}~\OPT{\NT{concl-occ}}
+\nlsep \KWD{in}~\OPT{\TERM{hyp-ident-list}} ~\KWD{$\vdash$} ~\OPT{\NT{concl-occ}}
 \nlsep \KWD{in}~\OPT{\TERM{hyp-ident-list}}
 \SEPDEF
 \DEFNT{hyp-ident-list}
-- 
cgit v1.2.3