2 files changed, 6 insertions, 0 deletions
diff --git a/kernel/names.ml b/kernel/names.ml
index 9267a64d61..d673c91e86 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -82,6 +82,9 @@ struct
   type t = Anonymous     (** anonymous identifier *)
 	 | Name of Id.t  (** non-anonymous identifier *)
 
+  let mk_name id =
+    Name id
+
   let is_anonymous = function
     | Anonymous -> true
     | Name _ -> false
diff --git a/kernel/names.mli b/kernel/names.mli
index feaedc775c..0af1cde8fb 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -82,6 +82,9 @@ sig
   type t = Anonymous     (** anonymous identifier *)
 	 | Name of Id.t  (** non-anonymous identifier *)
 
+  val mk_name : Id.t -> t
+  (** constructor *)
+
   val is_anonymous : t -> bool
   (** Return [true] iff a given name is [Anonymous]. *)