diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-05 18:13:48 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-05 18:13:48 +0000 |
| commit | f7b287e5a11d9905142527d0976afc32113e749d (patch) | |
| tree | d8c2eb762bef3d7d245550d0ef634608bf89e7d8 /doc/syntax-v8.tex | |
| parent | 0cb028c11465747ea4c29ba122f2aabfa40d7e64 (diff) | |
Oubli
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4814 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/syntax-v8.tex')
| -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 d59768f21..dfefabaf5 100644 --- a/doc/syntax-v8.tex +++ b/doc/syntax-v8.tex @@ -967,7 +967,7 @@ $$ \nlsep \TERM{SearchPattern}~\NT{constr-pattern}~\OPT{\NT{in-out-modules}} \nlsep \TERM{SearchRewrite}~\NT{constr-pattern}~\OPT{\NT{in-out-modules}} \nlsep \TERM{SearchAbout}~\NT{reference}~\OPT{\NT{in-out-modules}} -\nlsep \TERM{SearchAbout}~\TERM{[}~\NT{ref-or-string}~\TERM{]}\OPT{\NT{in-out-modules}} +\nlsep \TERM{SearchAbout}~\TERM{[}~\STAR{\NT{ref-or-string}}~\TERM{]}\OPT{\NT{in-out-modules}} \nlsep \KWD{Set}~\NT{ident}~\OPT{\NT{opt-value}} \nlsep \TERM{Unset}~\NT{ident} \nlsep \KWD{Set}~\NT{ident}~\NT{ident}~\OPT{\NT{opt-value}} |