diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/ide_blob.ml | 1 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 6 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 7 |
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 |