From f7b287e5a11d9905142527d0976afc32113e749d Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 5 Nov 2003 18:13:48 +0000 Subject: Oubli git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4814 85f007b7-540e-0410-9357-904b9bb8a0f7 --- doc/syntax-v8.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc/syntax-v8.tex') 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}} -- cgit v1.2.3