diff options
Diffstat (limited to 'library/lib.ml')
| -rw-r--r-- | library/lib.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/library/lib.ml b/library/lib.ml index 323ca60de..243fc1aca 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -471,12 +471,12 @@ let reset_to sp = let (after,_,_) = split_lib spf in recache_context after -let reset_name id = +let reset_name (loc,id) = let (sp,_) = try find_entry_p (fun (sp,_) -> let (_,spi) = repr_path (fst sp) in id = spi) with Not_found -> - error (string_of_id id ^ ": no such entry") + user_err_loc (loc,"reset_name",pr_id id ++ str ": no such entry") in reset_to sp |