diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-29 13:54:31 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-29 13:54:31 +0000 |
| commit | 8ad2e69d44c128ee9c22be462e0b538fbfa25aec (patch) | |
| tree | c55dfa623f1f6950feee0116eb445bd0f7e9dcac /doc | |
| parent | 5a3ec7aaf5b5f6751b2fd943767423047e2a8d00 (diff) | |
Bugs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3195 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/newsyntax.tex | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/newsyntax.tex b/doc/newsyntax.tex index e02a1b5b6..79d680fcb 100644 --- a/doc/newsyntax.tex +++ b/doc/newsyntax.tex @@ -575,7 +575,7 @@ $identificateur$ & $module$ & $infixe/préfixe$ & $précédence$ \\ \texttt{Rgt} & $Rdefinitions$ & $>$ & 50 \\ \texttt{plus} & $Peano$ & + & 40\,L \\ \texttt{Zplus} & $fast_integer$ & + & 40\,L \\ -\texttt{Rplus} & $fast_integer$ & + & 40\,L \\ +\texttt{Rplus} & $Rdefinitions$ & + & 40\,L \\ \texttt{minus} & $Minus$ & - & 40\,L \\ \texttt{Zminus} & $zarith_aux$ & - & 40\,L \\ \texttt{Rminus} & $Rdefinitions$ & - & 40\,L \\ @@ -586,6 +586,7 @@ $identificateur$ & $module$ & $infixe/préfixe$ & $précédence$ \\ \texttt{Rmult} & $Rdefinitions$ & * & 30\,L \\ \texttt{Rdiv} & $Rdefinitions$ & / & 30\,L \\ \texttt{pow} & $Rfunctions$ & \hat & 20\,L \\ +\texttt{fact} & $Rfunctions$ & ! & 20\,L \\ \end{array} $$ |