From 2c18da20b260c55d8da49b1bb4f53e72dbc75a87 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Wed, 24 Apr 2019 11:37:42 +0000
Subject: Revert #9249

---
 lib/util.mli | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'lib/util.mli')

diff --git a/lib/util.mli b/lib/util.mli
index fa3b622621..1eb60f509a 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -17,10 +17,6 @@ val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c
 val on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b
 val map_pair : ('a -> 'b) -> 'a * 'a -> 'b * 'b
 
-(** Comparing pairs *)
-
-val pair_compare : ('a -> 'a -> int) -> ('b -> 'b -> int) -> ('a * 'b -> 'a * 'b -> int)
-
 (** Mapping under triple *)
 
 val on_pi1 : ('a -> 'b) -> 'a * 'c * 'd -> 'b * 'c * 'd
-- 
cgit v1.2.3