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/ppvernac.ml | |
| 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/ppvernac.ml')
| -rw-r--r-- | parsing/ppvernac.ml | 7 |
1 files changed, 0 insertions, 7 deletions
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 |