diff options
| -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 e02a1b5b67..79d680fcb9 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} $$ |