diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-23 16:49:49 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-23 16:49:49 +0000 |
| commit | 5c915de161fe453914525e5920d1a165bba8fa43 (patch) | |
| tree | c079616f63c212bb8adec15a5361fad1955419f4 /library/lib.mli | |
| 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 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/library/lib.mli b/library/lib.mli index 0a445f076..df931f060 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -155,7 +155,6 @@ val close_section : unit -> unit val reset_to : Libnames.object_name -> unit val reset_name : Names.identifier Pp.located -> unit -val remove_name : Names.identifier Pp.located -> unit val reset_mod : Names.identifier Pp.located -> unit (** [back n] resets to the place corresponding to the {% $ %}n{% $ %}-th call of |