aboutsummaryrefslogtreecommitdiff
path: root/library/libnames.mli
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-05-16 14:32:09 +0200
committerGaëtan Gilbert2019-05-16 15:40:50 +0200
commit11533785773269d9632ef8925ed34ea2d541818b (patch)
treea814044c27d45a10373c5a42739ad302c29e00ce /library/libnames.mli
parent21269d0fef6794a672c36abdc5760889adc0e09c (diff)
Fix #10176: shadowing vs automatic class based generalization
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 *)