diff options
Diffstat (limited to 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/library/lib.mli b/library/lib.mli index 0d6eb34b8..0a445f076 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -154,9 +154,9 @@ val close_section : unit -> unit (** {6 Backtracking (undo). } *) val reset_to : Libnames.object_name -> unit -val reset_name : Names.identifier Util.located -> unit -val remove_name : Names.identifier Util.located -> unit -val reset_mod : Names.identifier Util.located -> 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 [mark_end_of_command] (counting backwards) *) |