From 00cd350c772f2865cd61d2dcfd1cf843ee5f0d18 Mon Sep 17 00:00:00 2001
From: glondu
Date: Wed, 6 Oct 2010 08:49:55 +0000
Subject: Remove VernacGo

I agree with Arnaud on this one...

Archeology: I could trace it back to r133 (in 1999!), and it was
adapted to many big changes, including change of parsing (r2722, in
2002). Maybe it was used by Centaur or something similar once... The
only relevant occurrences of "Go" in SVN history (since initial commit
in 1999) is that it "semble peu robuste aux erreurs", without a clear
specification of what it is supposed to do...

Looks like an interesting feature, though, but needs complete
rethinking (and documentation) with the new engine.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13506 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/RefMan-oth.tex | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index d7208aee6a..c1dc35dcb9 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -972,9 +972,6 @@ This command displays the current nesting depth used for display.
 %\subsection{\tt Explain ...}
 %Not yet documented.
 
-%\subsection{\tt Go ...}
-%Not yet documented.
-
 %\subsection{\tt Abstraction ...}
 %Not yet documented.
 
-- 
cgit v1.2.3