aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/lib.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/lib.ml')
-rw-r--r--library/lib.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/library/lib.ml b/library/lib.ml
index ea8120787..075e0e12a 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -178,6 +178,7 @@ let reset_to sp =
let (after,_,_) = split_lib spf in
recache_context (List.rev after)
+let is_section_p sp = list_prefix_of (wd_of_sp sp) !path_prefix
(* State and initialization. *)