aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--library/lib.ml3
1 files changed, 1 insertions, 2 deletions
diff --git a/library/lib.ml b/library/lib.ml
index f713d0414e..b8e7cea951 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -627,8 +627,7 @@ let library_part ref =
let dir,_ = repr_path sp in
match ref with
| VarRef id ->
- anomaly "TODO";
- extract_dirpath_prefix (sections_depth ()) (cwd ())
+ anomaly "library_part not supported on local variables"
| _ ->
if is_dirpath_prefix_of dir (cwd ()) then
(* Not yet (fully) discharged *)