diff options
| author | marche | 2003-12-19 09:19:09 +0000 |
|---|---|---|
| committer | marche | 2003-12-19 09:19:09 +0000 |
| commit | 99e2f370a25f126f036b2910d4b919951002fb91 (patch) | |
| tree | bc19463d6b931d6277beeb49c195e34af78dbea6 /doc/RefMan-syn.tex | |
| parent | a1fa5ceaf8e084411ce60bf5e38b24ee4e857f6d (diff) | |
COQBIN plus necessaire, typos
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8417 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/RefMan-syn.tex')
| -rwxr-xr-x | doc/RefMan-syn.tex | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/doc/RefMan-syn.tex b/doc/RefMan-syn.tex index 78ba6cc92b..d5604ecc44 100755 --- a/doc/RefMan-syn.tex +++ b/doc/RefMan-syn.tex @@ -125,10 +125,10 @@ necessarily parsed surrounded by parentheses. notation & precedence/associativity \\ \hline \verb$"_ , _"$ & 250 \\ -\verb$exists _ : _ | _$ & 200 \\ -\verb$exists _ | _$ & 200 \\ -\verb$exists2 _ : _ | _ & _$ & 200 \\ -\verb$exists2 _ | _ & _$ & 200 \\ +\verb$exists _ : _, _$ & 200 \\ +\verb$exists _, _$ & 200 \\ +\verb$exists2 _ : _, _ & _$ & 200 \\ +\verb$exists2 _, _ & _$ & 200 \\ \verb$"_ <-> _"$ & 95 \\ \verb$"_ -> _"$ & 90\, R (primitive) \\ \verb$"_ \/ _"$ & 85\, R \\ @@ -153,7 +153,7 @@ notation & precedence/associativity \\ \verb$"_ / _"$ & 40\, L \\ \verb$"- _"$ & 35\, R \\ \verb$"/ _"$ & 35\, R \\ -\verb$"_ ^ _"$ & 30\, L \\ +\verb$"_ ^ _"$ & 30\, R \\ \verb$"{ _ } + { _ }"$ & 0 \\ \verb$"_ + { _ }"$ & 50\, L \\ \verb$"{ _ : _ | _ }"$ & 0 \\ @@ -389,7 +389,7 @@ notation are replaced by ``\_''. \begin{coq_example} Locate "exists". -Locate "'exists' _ | _". +Locate "'exists' _ , _". \end{coq_example} \SeeAlso Section \ref{Locate}. |