aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/names.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/names.mli')
-rw-r--r--kernel/names.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/names.mli b/kernel/names.mli
index 417e35aaa..16d0ae5d0 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -46,6 +46,9 @@ sig
module Pred : Predicate.S with type elt = t
(** Predicates over identifiers. *)
+ module List : List.MonoS with type elt = t
+ (** Operations over lists of identifiers. *)
+
val hcons : t -> t
(** Hashconsing of identifiers. *)