From 2fe6aa3b4d422ec092844e84c4d15f5c1414b442 Mon Sep 17 00:00:00 2001
From: glondu
Date: Wed, 6 Oct 2010 18:57:04 +0000
Subject: 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
---
 dev/v8-syntax/syntax-v8.tex | 2 --
 1 file changed, 2 deletions(-)

(limited to 'dev/v8-syntax')

diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex
index 46ba24da70..4fb47bea7b 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}
-- 
cgit v1.2.3