From 67319cef77a215163032ea94f28f8c21dcf64f3a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Thu, 20 Mar 2014 15:27:40 +0100
Subject: Missing equalities in Names-like structures.

---
 library/globnames.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'library/globnames.mli')

diff --git a/library/globnames.mli b/library/globnames.mli
index 4569d8e1f..0a7bf850c 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -77,6 +77,7 @@ type extended_global_reference =
 module ExtRefOrdered : sig
   type t = extended_global_reference
   val compare : t -> t -> int
+  val equal : t -> t -> bool
   val hash : t -> int
 end
 
-- 
cgit v1.2.3