diff options
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 |