aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-06-21 15:23:58 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-08-01 19:26:33 +0200
commit98af6dfee8ec5a03580cf580d7e09b3e49265322 (patch)
tree585885eebb018e058c6888fbaf275c8358da911a
parentc720b6f20a4bef54c570d9a3002938828779654b (diff)
Fix syntax-v8.tex bad parenthesizing
-rw-r--r--dev/v8-syntax/syntax-v8.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex
index fa2864cec..6b7960c92 100644
--- a/dev/v8-syntax/syntax-v8.tex
+++ b/dev/v8-syntax/syntax-v8.tex
@@ -1158,7 +1158,7 @@ $$
\nlsep \TERM{Abort}~\NT{ident}
\nlsep \TERM{Existential}~\NT{num}~\KWD{:=}~\NT{constr-body}
\nlsep \TERM{Qed}
-\nlsep \TERM{Save}~\NT{ident}}
+\nlsep \TERM{Save}~\NT{ident}
\nlsep \TERM{Defined}~\OPT{\NT{ident}}
\nlsep \TERM{Suspend}
\nlsep \TERM{Resume}~\OPT{\NT{ident}}