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/names.ml | |
| 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/names.ml')
| -rw-r--r-- | kernel/names.ml | 8 |
1 files changed, 6 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 |