From 7b7187ab30c945f7929299833a92ee01737519a6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Mon, 3 Mar 2014 03:42:49 +0100
Subject: Goptions do not rely anymore on generic equality.

---
 pretyping/detyping.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'pretyping/detyping.mli')

diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 97c636af7..8a10b7ed5 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -72,6 +72,7 @@ module PrintingInductiveMake :
   end) ->
     sig
       type t = Names.inductive
+      val compare : t -> t -> int
       val encode : Libnames.reference -> Names.inductive
       val subst : substitution -> t -> t
       val printer : t -> Pp.std_ppcmds
-- 
cgit v1.2.3