diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-02-18 18:32:33 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-02-18 18:32:33 +0000 |
| commit | b5df1925bbc14f441247349b200aa3f5828e8427 (patch) | |
| tree | c158ac5d3d3133f2fce8188f3d0b4a75bd0c5415 /doc | |
| parent | 06900e469cd593c272f57c2af7d2e4f206a2f944 (diff) | |
- 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
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/syntax-v8.tex | 2 |
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}} |