aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/v8-syntax
diff options
context:
space:
mode:
Diffstat (limited to 'dev/v8-syntax')
-rw-r--r--dev/v8-syntax/syntax-v8.tex2
1 files changed, 0 insertions, 2 deletions
diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex
index 46ba24da7..4fb47bea7 100644
--- a/dev/v8-syntax/syntax-v8.tex
+++ b/dev/v8-syntax/syntax-v8.tex
@@ -1179,8 +1179,6 @@ $$
\nlsep \TERM{Show}~\TERM{Intros}
%% Correctness: obsolete ?
%%\nlsep \TERM{Show}~\TERM{Programs}
-\nlsep \TERM{Explain}~\TERM{Proof}~\OPT{\TERM{Tree}}~\STAR{\NT{num}}
-%% Go not documented
\nlsep \TERM{Hint}~\OPT{\TERM{Local}}~\NT{hint}~\OPT{\NT{inbases}}
%% PrintConstr not documented
\end{rules}