diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-06 08:49:55 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-06 08:49:55 +0000 |
| commit | 00cd350c772f2865cd61d2dcfd1cf843ee5f0d18 (patch) | |
| tree | 8b768ad6fce21e8d9bfcb5b51df9aec88fb5c351 /ide/ide.mllib | |
| 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 'ide/ide.mllib')
0 files changed, 0 insertions, 0 deletions