diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_proofs.ml4 | 4 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 7 |
2 files changed, 0 insertions, 11 deletions
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 |