aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
Diffstat (limited to 'doc')
-rw-r--r--doc/syntax-v8.tex5
1 files changed, 4 insertions, 1 deletions
diff --git a/doc/syntax-v8.tex b/doc/syntax-v8.tex
index 6f59f53f2d..454f87ca65 100644
--- a/doc/syntax-v8.tex
+++ b/doc/syntax-v8.tex
@@ -818,7 +818,10 @@ $$
\nlsep \NT{mod-type}~\KWD{with}~\NT{with-declaration}
\SEPDEF
\DEFNT{with-declaration}
- \TERM{Definition}~\NT{ident}~\KWD{:=}~\NTL{constr}{100}
+ %on forcera les ( )
+ %si exceptionnellemt
+ %un fixpoint ici
+ \TERM{Definition}~\NT{ident}~\KWD{:=}~\NTL{constr}{} %{100}
\nlsep \TERM{Module}~\NT{ident}~\KWD{:=}~\NT{reference}
\SEPDEF
\DEFNT{of-mod-type}