diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-16 11:00:44 +0100 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-18 15:57:16 +0100 |
| commit | e2a67cbbbd17fa262b37903a97b0adf2d109bf06 (patch) | |
| tree | 02b83911cbb2fd09a12361d21c56ed4ee1609be5 /kernel/names.ml | |
| parent | eee16239f6b00400c8a13b787c310bcb11c37afe (diff) | |
COMMENTS: added to the "Names" module.
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 } *) |