aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/syntax-v8.tex
diff options
context:
space:
mode:
Diffstat (limited to 'doc/syntax-v8.tex')
-rw-r--r--doc/syntax-v8.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/syntax-v8.tex b/doc/syntax-v8.tex
index 53e191e98..9eb3c7a63 100644
--- a/doc/syntax-v8.tex
+++ b/doc/syntax-v8.tex
@@ -1154,7 +1154,7 @@ $$
\nlsep \TERM{Proof}~\KWD{with}~\NT{tactic}
\nlsep \TERM{Abort}~\OPT{\TERM{All}}
\nlsep \TERM{Abort}~\NT{ident}
-\nlsep \TERM{Existential}~\NT{num}~\NT{constr-body}
+\nlsep \TERM{Existential}~\NT{num}~\KWD{:=}~\NT{constr-body}
\nlsep \TERM{Qed}
\nlsep \TERM{Save}~\OPTGR{\NT{thm-token}~\NT{ident}}
\nlsep \TERM{Defined}~\OPT{\NT{ident}}