Do NOT dare using Pervasives.compare on data structures containing URIs!

Use UriManager.compare to get a 2x speed-up in type-checking setoids.

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index 7aac62cff5b77e08ae1537ab2850731b52c9e27b..fe9f01d532af2c65866fb1b9a34d6cf223ed76dd 100644 (file)
--- 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)