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

3 files changed, 0 insertions, 14 deletions

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