diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-06 18:57:04 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-06 18:57:04 +0000 |
| commit | 2fe6aa3b4d422ec092844e84c4d15f5c1414b442 (patch) | |
| tree | 55b5e6255d514cc05b72b0041fd567dd0d11132d /dev/v8-syntax | |
| parent | b36e75cca2ea910dead09864c4f10ba79b894a35 (diff) | |
Remove Explain* vernacs
Basically untouched since 1999. Same fate as VernacGo (r13506).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13510 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/v8-syntax')
| -rw-r--r-- | dev/v8-syntax/syntax-v8.tex | 2 |
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} |