diff options
| author |  mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-27 12:42:06 +0000 |
|---|---|---|
| committer | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-27 12:42:06 +0000 |
| commit | 0ebf78fb3bf0300312c22ee708e111c0a2f4be30 (patch) | |
| tree | 5f36c0bb380e7ecc87075336851ac0186f3b3b87 /doc | |
| parent | 57a672130462d40deacaf462e32433f5adcfe888 (diff) | |
Reparation bug compil
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5005 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/syntax-v8.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/syntax-v8.tex b/doc/syntax-v8.tex index 76fe0e506..031f59885 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} |