diff options
Diffstat (limited to 'kernel/names.ml')
-rw-r--r-- | kernel/names.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index 9e4e8cd61..0de752c7c 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 } *) |