From b5df1925bbc14f441247349b200aa3f5828e8427 Mon Sep 17 00:00:00 2001
From: barras
Date: Wed, 18 Feb 2004 18:32:33 +0000
Subject: - fixed the Assert_failure error in kernel/modops - fixed the problem
 with passing atomic tactics to ltacs - restructured the distrib Makefile (can
 build a package from   the CVS working dir)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5358 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/syntax-v8.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/syntax-v8.tex b/doc/syntax-v8.tex
index 53e191e98f..9eb3c7a636 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}}
-- 
cgit v1.2.3