From 663922262bc9bcc8876f7e12910f6294fc964753 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Wed, 24 Aug 2016 15:31:28 +0200
Subject: Changing the definition of the "Lib.variable.info" type to enable us
 to do more cleanups

---
 kernel/names.ml  | 3 +++
 kernel/names.mli | 3 +++
 2 files changed, 6 insertions(+)

(limited to 'kernel')

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]. *)
 
-- 
cgit v1.2.3