diff options
| author | letouzey | 2012-03-23 16:49:49 +0000 |
|---|---|---|
| committer | letouzey | 2012-03-23 16:49:49 +0000 |
| commit | 5c915de161fe453914525e5920d1a165bba8fa43 (patch) | |
| tree | c079616f63c212bb8adec15a5361fad1955419f4 /kernel/type_errors.ml | |
| parent | 3d1124c0acc9a126624a4ea6e71116fa8959b06b (diff) | |
Remove undocumented command "Delete foo"
This command isn't trivial to port to the forthcoming evolution of
backtracking in coqtop. Moreover, it isn't clear whether this
"Delete" works well in advanced situation (was not updating
frozen states).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15084 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions