aboutsummaryrefslogtreecommitdiff
path: root/library/libnames.ml
diff options
context:
space:
mode:
authorHugo Herbelin2019-05-22 18:12:36 +0200
committerHugo Herbelin2019-05-22 18:12:36 +0200
commit5c5bd952e9c28c3acf740fcdced03b2b7145076d (patch)
treea56647f099136d571f2f2c6c47ddb31472ef7804 /library/libnames.ml
parent4f2e05f5abc19addc25501281b4cd34ed5e33853 (diff)
parent28dfb113c19f467fdc2b785d1c5a07a42aefa488 (diff)
Merge PR #10177: Fix #10176: shadowing vs automatic class based generalization + cleanups
Reviewed-by: herbelin
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"] *)