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

6 files changed, 0 insertions, 28 deletions

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.
 
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index d9f8d7a900..b5bac26c3f 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -84,10 +84,6 @@ GEXTEND Gram
 	  VernacShow (ExplainProof l)
       | IDENT "Explain"; IDENT "Proof"; IDENT "Tree"; l = LIST0 integer ->
 	  VernacShow (ExplainTree l)
-      | IDENT "Go"; n = natural -> VernacGo (GoTo n)
-      | IDENT "Go"; IDENT "top" -> VernacGo GoTop
-      | IDENT "Go"; IDENT "prev" -> VernacGo GoPrev
-      | IDENT "Go"; IDENT "next" -> VernacGo GoNext
       | IDENT "Guarded" -> VernacCheckGuard
 (* Hints for Auto and EAuto *)
       | IDENT "Create"; IDENT "HintDb" ;
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 269f816994..24c9d9d8ac 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -451,13 +451,6 @@ let rec pr_vernac = function
   | VernacBacktrack (i,j,k) ->
       str "Backtrack" ++  spc() ++ prlist_with_sep sep int [i;j;k]
   | VernacFocus i -> str"Focus" ++ pr_opt int i
-  | VernacGo g ->
-      let pr_goable = function
-	| GoTo i -> int i
-	| GoTop -> str"top"
-	| GoNext -> str"next"
-	| GoPrev -> str"prev"
-      in str"Go" ++ spc() ++  pr_goable g
   | VernacShow s ->
       let pr_showable = function
 	| ShowGoal n -> str"Show" ++ pr_opt int n
diff --git a/toplevel/ide_blob.ml b/toplevel/ide_blob.ml
index 8df17350c7..b90b44687c 100644
--- a/toplevel/ide_blob.ml
+++ b/toplevel/ide_blob.ml
@@ -156,7 +156,6 @@ let rec attribute_of_vernac_command = function
   
   | VernacFocus _ -> [SolveCommand]
   | VernacUnfocus -> [SolveCommand]
-  | VernacGo _ -> []
   | VernacShow _ -> [OtherStatePreservingCommand]
   | VernacCheckGuard -> [OtherStatePreservingCommand]
   | VernacProof (Tacexpr.TacId []) -> [OtherStatePreservingCommand]
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index c6071eb966..7d342737c7 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1237,11 +1237,6 @@ let vernac_end_subproof () =
   let p = Proof_global.give_me_the_proof () in
   Proof.unfocus subproof_kind p ; print_subgoals ()
 
-let vernac_go _ = 
-  (* spiwack: don't know what it's supposed to do. Undocumented. 
-     Deactivated and candidate for removal. (Feb. 2010) *)
-  ()
-
 let explain_proof occ =
   (* spiwack: don't know what it's supposed to do. Undocumented. 
      Deactivated and candidate for removal. (Feb. 2010) *)
@@ -1405,7 +1400,6 @@ let interp c = match c with
   | VernacUnfocus -> vernac_unfocus ()
   | VernacSubproof n -> vernac_subproof n
   | VernacEndSubproof -> vernac_end_subproof ()
-  | VernacGo g -> vernac_go g
   | VernacShow s -> vernac_show s
   | VernacCheckGuard -> vernac_check_guard ()
   | VernacProof tac -> vernac_set_end_tac tac
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 50fb61ebad..f3aa076ada 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -81,12 +81,6 @@ type locatable =
   | LocateTactic of reference
   | LocateFile of string
 
-type goable =
-  | GoTo of int
-  | GoTop
-  | GoNext
-  | GoPrev
-
 type showable =
   | ShowGoal of int option
   | ShowGoalImplicitly of int option
@@ -344,7 +338,6 @@ type vernac_expr =
   | VernacUnfocus
   | VernacSubproof of int option
   | VernacEndSubproof
-  | VernacGo of goable
   | VernacShow of showable
   | VernacCheckGuard
   | VernacProof of raw_tactic_expr