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 /parsing | |
| 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 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 1 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 1 |
2 files changed, 0 insertions, 2 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 9b66cacb16..38e4e8eec1 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -931,7 +931,6 @@ GEXTEND Gram (* Resetting *) | IDENT "Reset"; id = identref -> VernacResetName id - | IDENT "Delete"; id = identref -> VernacRemoveName id | IDENT "Reset"; IDENT "Initial" -> VernacResetInitial | IDENT "Back" -> VernacBack 1 | IDENT "Back"; n = natural -> VernacBack n diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index c4ffbfd152..49c76c96ce 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -471,7 +471,6 @@ let rec pr_vernac = function | VernacCheckGuard -> str"Guarded" (* Resetting *) - | VernacRemoveName id -> str"Remove" ++ spc() ++ pr_lident id | VernacResetName id -> str"Reset" ++ spc() ++ pr_lident id | VernacResetInitial -> str"Reset Initial" | VernacBack i -> if i=1 then str"Back" else str"Back" ++ pr_intarg i |