2 files changed, 9 insertions, 2 deletions
diff --git a/kernel/names.ml b/kernel/names.ml
index afdbe0c0dc..ae34033355 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -104,8 +104,12 @@ struct
     | _ -> false
 
   let hash = function
-  | Anonymous -> 0
-  | Name id -> Id.hash id
+    | Anonymous -> 0
+    | Name id -> Id.hash id
+
+  let print = function
+    | Anonymous -> str "_"
+    | Name id -> Id.print id
 
   module Self_Hashcons =
     struct
diff --git a/kernel/names.mli b/kernel/names.mli
index 5b0163aa55..c73eb197bb 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -105,6 +105,9 @@ sig
   val hcons : t -> t
   (** Hashconsing over names. *)
 
+  val print : t -> Pp.std_ppcmds
+  (** Pretty-printer (print "_" for [Anonymous]. *)
+
 end
 
 (** {6 Type aliases} *)