aboutsummaryrefslogtreecommitdiff
path: root/library/libnames.mli
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.mli
parent4f2e05f5abc19addc25501281b4cd34ed5e33853 (diff)
parent28dfb113c19f467fdc2b785d1c5a07a42aefa488 (diff)
Merge PR #10177: Fix #10176: shadowing vs automatic class based generalization + cleanups
Reviewed-by: herbelin
Diffstat (limited to 'library/libnames.mli')
-rw-r--r--library/libnames.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/library/libnames.mli b/library/libnames.mli
index bbb4d2a058..7d77d95991 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -88,6 +88,9 @@ val qualid_is_ident : qualid -> bool
val qualid_path : qualid -> DirPath.t
val qualid_basename : qualid -> Id.t
+val idset_mem_qualid : qualid -> Id.Set.t -> bool
+(** false when the qualid is not an ident *)
+
(** {6 ... } *)
(** some preset paths *)