aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/v8-syntax
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-03-20 01:22:58 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-03-20 01:22:58 +0000
commit7d220f8b61649646692983872626d6a8042446a9 (patch)
treefefceb2c59cf155c55fffa25ad08bec629de523e /dev/v8-syntax
parentad1fea78e3c23c903b2256d614756012d5f05d87 (diff)
Directory 'contrib' renamed into 'plugins', to end confusion with archive of user contribs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/v8-syntax')
-rw-r--r--dev/v8-syntax/syntax-v8.tex18
1 files changed, 9 insertions, 9 deletions
diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex
index de68ce1e5..46ba24da7 100644
--- a/dev/v8-syntax/syntax-v8.tex
+++ b/dev/v8-syntax/syntax-v8.tex
@@ -744,28 +744,28 @@ Conflicts exists between integers and constrs.
\nlsep \TERM{simplif}
\nlsep \TERM{intuition}~\OPT{\NTL{tactic}{0}}
\nlsep \TERM{linearintuition}~\OPT{\NT{num}}
-%% contrib/cc
+%% plugins/cc
\nlsep \TERM{cc}
-%% contrib/field
+%% plugins/field
\nlsep \TERM{field}~\STAR{\tacconstr}
-%% contrib/firstorder
+%% plugins/firstorder
\nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}
\nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}~\KWD{with}~\PLUS{\NT{reference}}
\nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}~\KWD{using}~\PLUS{\NT{ident}}
%%\nlsep \TERM{gtauto}
\nlsep \TERM{gintuition}~\OPT{\NTL{tactic}{0}}
-%% contrib/fourier
+%% plugins/fourier
\nlsep \TERM{fourierZ}
-%% contrib/funind
+%% plugins/funind
\nlsep \TERM{functional}~\TERM{induction}~\tacconstr~\PLUS{\tacconstr}
-%% contrib/jprover
+%% plugins/jprover
\nlsep \TERM{jp}~\OPT{\NT{num}}
-%% contrib/omega
+%% plugins/omega
\nlsep \TERM{omega}
-%% contrib/ring
+%% plugins/ring
\nlsep \TERM{quote}~\NT{ident}~\OPTGR{\KWD{[}~\PLUS{\NT{ident}}~\KWD{]}}
\nlsep \TERM{ring}~\STAR{\tacconstr}
-%% contrib/romega
+%% plugins/romega
\nlsep \TERM{romega}
\SEPDEF
\DEFNT{orient}