From 70d8c1e7a24b542c8e3f1788fd18226e2469801b Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 1 Mar 2012 18:59:02 +0000
Subject: Univ: a better Constraint.compare

Let's gain a few % by not using Pervasive.compare on a structure containing
some universe_levels, but rather UniverseLevel.compare on them.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15012 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/univ.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index e4c2a5034c..1aad0fce14 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -491,7 +491,13 @@ let enforce_constraint cst g =
 module Constraint = Set.Make(
   struct
     type t = univ_constraint
-    let compare = Pervasives.compare
+    let compare (u,c,v) (u',c',v') =
+      let i = Pervasives.compare c c' in
+      if i <> 0 then i
+      else
+	let i' = UniverseLevel.compare u u' in
+	if i' <> 0 then i'
+	else UniverseLevel.compare v v'
   end)
 
 type constraints = Constraint.t
-- 
cgit v1.2.3