COMMENTS: added to the "Names" module.

1 files changed, 17 insertions, 12 deletions

diff --git a/kernel/names.mli b/kernel/names.mli
index c5a7d8f3c..b128fe335 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -10,30 +10,33 @@ open Util
 
 (** {6 Identifiers } *)
 
+(** Representation and operations on identifiers. *)
 module Id :
 sig
   type t
-  (** Type of identifiers *)
+  (** Values of this type represent (Coq) identifiers. *)
 
   val equal : t -> t -> bool
-  (** Equality over identifiers *)
+  (** Equality over identifiers. *)
 
   val compare : t -> t -> int
-  (** Comparison over identifiers *)
+  (** Comparison over identifiers. *)
 
   val hash : t -> int
-  (** Hash over identifiers *)
+  (** Hash over identifiers. *)
 
   val is_valid : string -> bool
-  (** Check that a string may be converted to an identifier. *)
+  (** Check that a string may be converted to an identifier.
+  @raise Unicode.Unsupported if the provided string contains unsupported UTF-8 characters. *)
 
   val of_string : string -> t
-  (** Converts a string into an identifier. May raise [UserError _] if the
-      string is not valid, or echo a warning if it contains invalid identifier
-      characters. *)
+  (** Converts a string into an identifier.
+      @raise UserError if the string is not valid, or echo a warning if it contains invalid identifier characters.
+      @raise Unicode.Unsupported if the provided string contains unsupported UTF-8 characters. *)
 
   val of_string_soft : string -> t
-  (** Same as {!of_string} except that no warning is ever issued. *)
+  (** Same as {!of_string} except that no warning is ever issued.
+      @raise Unicode.Unsupported if the provided string contains unsupported UTF-8 characters. *)
 
   val to_string : t -> string
   (** Converts a identifier into an string. *)
@@ -58,10 +61,12 @@ sig
 
 end
 
+(** Representation and operations on identifiers that are allowed to be anonymous
+    (i.e. "_" in concrete syntax). *)
 module Name :
 sig
-  type t = Name of Id.t | Anonymous
-  (** A name is either undefined, either an identifier. *)
+  type t = Anonymous     (** anonymous identifier *)
+	 | Name of Id.t  (** non-anonymous identifier *)
 
   val compare : t -> t -> int
   (** Comparison over names. *)
@@ -79,7 +84,7 @@ end
 
 (** {6 Type aliases} *)
 
-type name = Name.t = Name of Id.t | Anonymous
+type name = Name.t = Anonymous | Name of Id.t
 type variable = Id.t
 type module_ident = Id.t