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 ++++++
 kernel/names.mli | 6 ++++++
 2 files changed, 12 insertions(+)

(limited to 'kernel')

diff --git a/kernel/names.ml b/kernel/names.ml
index 02587bad9b..0aa26fb9cc 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
diff --git a/kernel/names.mli b/kernel/names.mli
index 40f96813fc..6380b17fbf 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -68,6 +68,12 @@ sig
   type t = Anonymous     (** anonymous identifier *)
 	 | Name of Id.t  (** non-anonymous identifier *)
 
+  val is_anonymous : t -> bool
+  (** Return [true] iff a given name is [Anonymous]. *)
+
+  val is_name : t -> bool
+  (** Return [true] iff a given name is [Name _]. *)
+
   val compare : t -> t -> int
   (** Comparison over names. *)
 
-- 
cgit v1.2.3