diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-13 21:41:41 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-31 01:38:53 +0200 |
| commit | 8ab00e5f272aa8f16d70a00323c57f2d4ef66f03 (patch) | |
| tree | 337344749e72cc85334bfb56769272edf3e9b21d /kernel | |
| parent | 4865160fa1f2e9ce03b37b9cb3ac99c35e9c4e4d (diff) | |
Creating a module Nameops.Name extending module Names.Name.
This module collects the functions of Nameops which are about Name.t
and somehow standardize or improve their name, resulting in particular
from discussions in working group.
Note the use of a dedicated exception rather than a failwith for
Nameops.Name.out.
Drawback of the approach: one needs to open Nameops, or to use long
prefix Nameops.Name.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/names.ml | 8 | ||||
| -rw-r--r-- | kernel/names.mli | 3 |
2 files changed, 9 insertions, 2 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index afdbe0c0d..ae3403335 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -104,8 +104,12 @@ struct | _ -> false let hash = function - | Anonymous -> 0 - | Name id -> Id.hash id + | Anonymous -> 0 + | Name id -> Id.hash id + + let print = function + | Anonymous -> str "_" + | Name id -> Id.print id module Self_Hashcons = struct diff --git a/kernel/names.mli b/kernel/names.mli index 5b0163aa5..c73eb197b 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -105,6 +105,9 @@ sig val hcons : t -> t (** Hashconsing over names. *) + val print : t -> Pp.std_ppcmds + (** Pretty-printer (print "_" for [Anonymous]. *) + end (** {6 Type aliases} *) |