From ffb47b4d67608653c1ae024c5b291db8b209dddb Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Sun, 12 May 2013 15:54:13 +0000
Subject: Removing Gmap from Extraction plugin

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16511 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/names.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel')

diff --git a/kernel/names.mli b/kernel/names.mli
index f9fe89cde2..4b20b1c73a 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -124,6 +124,9 @@ sig
   val equal : t -> t -> bool
   (** Equality over labels *)
 
+  val compare : t -> t -> int
+  (** Comparison over labels. *)
+
   val make : string -> t
   (** Create a label out of a string. *)
 
-- 
cgit v1.2.3