From e2a67cbbbd17fa262b37903a97b0adf2d109bf06 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Wed, 16 Dec 2015 11:00:44 +0100
Subject: COMMENTS: added to the "Names" module.

---
 kernel/names.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'kernel/names.ml')

diff --git a/kernel/names.ml b/kernel/names.ml
index 9e4e8cd61d..0de752c7c5 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -23,6 +23,7 @@ open Util
 
 (** {6 Identifiers } *)
 
+(** Representation and operations on identifiers. *)
 module Id =
 struct
   type t = string
@@ -74,10 +75,12 @@ struct
 
 end
 
-
+(** Representation and operations on identifiers that are allowed to be anonymous
+    (i.e. "_" in concrete syntax). *)
 module Name =
 struct
-  type t = Name of Id.t | Anonymous
+  type t = Anonymous     (** anonymous identifier *)
+	 | Name of Id.t  (** non-anonymous identifier *)
 
   let compare n1 n2 = match n1, n2 with
     | Anonymous, Anonymous -> 0
@@ -117,8 +120,8 @@ struct
 
 end
 
-type name = Name.t = Name of Id.t | Anonymous
 (** Alias, to import constructors. *)
+type name = Name.t = Anonymous | Name of Id.t
 
 (** {6 Various types based on identifiers } *)
 
-- 
cgit v1.2.3