aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-04-13 21:41:41 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-05-31 01:38:53 +0200
commit8ab00e5f272aa8f16d70a00323c57f2d4ef66f03 (patch)
tree337344749e72cc85334bfb56769272edf3e9b21d /kernel
parent4865160fa1f2e9ce03b37b9cb3ac99c35e9c4e4d (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.ml8
-rw-r--r--kernel/names.mli3
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} *)