diff options
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 3 | ||||
| -rw-r--r-- | parsing/g_proofs.ml4 | 4 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 7 | ||||
| -rw-r--r-- | toplevel/ide_blob.ml | 1 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 6 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 7 |
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 |