From e4c9dfe7277ec2e2c4b1e40f60044ba4cade8e61 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Thu, 18 Feb 2016 14:19:21 +0100 Subject: ADD: Names.Name.is_{anonymous,name} Two new (trivial) functions were added: Names.Name.is_anonymous : Names.Name.t -> bool Names.Name.is_name : Names.Name.t -> bool They enable us to write a more compact code. (example: commit "99633f4" in "relation-extraction" module of "coq-contribs"). --- kernel/names.ml | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'kernel/names.ml') diff --git a/kernel/names.ml b/kernel/names.ml index 02587bad9..0aa26fb9c 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -82,6 +82,12 @@ struct type t = Anonymous (** anonymous identifier *) | Name of Id.t (** non-anonymous identifier *) + let is_anonymous = function + | Anonymous -> true + | Name _ -> false + + let is_name = not % is_anonymous + let compare n1 n2 = match n1, n2 with | Anonymous, Anonymous -> 0 | Name id1, Name id2 -> Id.compare id1 id2 -- cgit v1.2.3