From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- dev/v8-syntax/syntax-v8.tex | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'dev/v8-syntax') diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex index de68ce1e..46ba24da 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} -- cgit v1.2.3