aboutsummaryrefslogtreecommitdiff
path: root/library/libnames.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/libnames.ml')
-rw-r--r--library/libnames.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/library/libnames.ml b/library/libnames.ml
index 87c4de42e8..41b38e0378 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -162,6 +162,9 @@ let qualid_basename qid =
let qualid_path qid =
qid.CAst.v.dirpath
+let idset_mem_qualid qid s =
+ qualid_is_ident qid && Id.Set.mem (qualid_basename qid) s
+
(* Default paths *)
let default_library = Names.DirPath.initial (* = ["Top"] *)