diff options
| author | glondu | 2010-10-06 08:49:55 +0000 |
|---|---|---|
| committer | glondu | 2010-10-06 08:49:55 +0000 |
| commit | 00cd350c772f2865cd61d2dcfd1cf843ee5f0d18 (patch) | |
| tree | 8b768ad6fce21e8d9bfcb5b51df9aec88fb5c351 /parsing | |
| parent | a4347448697b26f77ea09d917144e2883c76d930 (diff) | |
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
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 |