From b6feaafc7602917a8ef86fb8adc9651ff765e710 Mon Sep 17 00:00:00 2001 From: Matej Košík Date: Mon, 29 May 2017 11:02:06 +0200 Subject: Remove (useless) aliases from the API. --- vernac/search.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/search.ml') diff --git a/vernac/search.ml b/vernac/search.ml index 916015800..0ff78f439 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -142,7 +142,7 @@ module ConstrPriority = struct -(3*(num_symbols t) + size t) let compare (_,_,_,p1) (_,_,_,p2) = - compare p1 p2 + Pervasives.compare p1 p2 end module PriorityQueue = Heap.Functional(ConstrPriority) -- cgit v1.2.3