From 0805c61933df87f5cfae63b94456a1f0518b06d0 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 23 Apr 2008 08:04:53 +0000
Subject: [PATCH] Do NOT dare using Pervasives.compare on data structures
 containing URIs! Use UriManager.compare to get a 2x speed-up in type-checking
 setoids.

---
 helm/software/components/cic/cicUniv.ml | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index 7aac62cff..fe9f01d53 100644
--- a/helm/software/components/cic/cicUniv.ml
+++ b/helm/software/components/cic/cicUniv.ml
@@ -50,7 +50,15 @@ type universe = int * UriManager.uri option
     
 module UniverseType = struct
   type t = universe
-  let compare = Pervasives.compare
+  let compare (n1,u1) (n2,u2) =
+   let ndiff = n1 - n2 in
+    if ndiff <> 0 then ndiff
+    else
+     match u1,u2 with
+        None, None -> 0
+      | Some u1, Some u2 -> UriManager.compare u1 u2
+      | None, Some _ -> 1
+      | Some _, None -> -1
 end
   
 module SOF = Set.Make(UniverseType)
-- 
2.39.2